PartialEquivBEq.trans
theorem PartialEquivBEq.trans :
∀ {α : Type u_1} [inst : BEq α] [self : PartialEquivBEq α] {a b c : α},
(a == b) = true → (b == c) = true → (a == c) = true
This theorem states the transitivity property for the function `BEq` in the context of a partial equivalence. In other words, for any type `α` with an instance of `BEq` and `PartialEquivBEq`, if `a`, `b`, and `c` are values of type `α`, and if `a` is equivalent to `b` and `b` is equivalent to `c` (expressed as `(a == b) = true` and `(b == c) = true`), then `a` is equivalent to `c` (expressed as `(a == c) = true`). This is a fundamental property of equivalence relations in mathematics.
More concisely: If `BEq` is an equivalence relation on type `α` with partial equivalence `PartialEquivBEq`, then `(a == b) and (b == c)` implies `(a == c)` for all `a, b, c : α`.
|
PartialEquivBEq.symm
theorem PartialEquivBEq.symm :
∀ {α : Type u_1} [inst : BEq α] [self : PartialEquivBEq α] {a b : α}, (a == b) = true → (b == a) = true
This theorem describes the symmetry property for the BEq operation in Lean. It states that for any type `α` that is equipped with a BEq operation (which compares two objects of type `α` for Boolean equality) and a PartialEquivBEq operation, if object `a` is Boolean-equal to object `b` (`a == b` is true), then object `b` is also Boolean-equal to object `a` (`b == a` is true). This symmetry property is a key characteristic of equivalence relations.
More concisely: If `α` has a BEq and a PartialEquivBEq relation, then `a BEq b` implies `b BEq a`.
|