Quot.exact
theorem Quot.exact : ∀ {α : Type u} (r : α → α → Prop) {a b : α}, Quot.mk r a = Quot.mk r b → EqvGen r a b
This theorem, `Quot.exact`, states that for any type `α` and an equivalence relation `r` on `α`, if two quotient types created by `Quot.mk` with inputs `a` and `b` are equal, then `a` and `b` are `EqvGen` related with respect to `r`. In other words, it essentially says that if two quotient types are the same, then the original elements that were used to create those quotient types must be related by the equivalence relation `r` that defines the quotient space.
More concisely: If two quotient types created by an equivalence relation are equal in Lean, then the corresponding elements are related by the equivalence relation.
|
Quot.EqvGen_sound
theorem Quot.EqvGen_sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, EqvGen r a b → Quot.mk r a = Quot.mk r b := by
sorry
The theorem `Quot.EqvGen_sound` states that for any type `α` and any relation `r` on `α`, and for any elements `a` and `b` of type `α`, if `a` and `b` generate an equivalence relation under `r` (denoted as `EqvGen r a b`), then the quotient of `a` and `b` with respect to the relation `r` are equal. This theorem can be interpreted as saying that the process of forming quotients respects the generation of equivalence relations.
More concisely: If `a` and `b` generate an equivalence relation `r` on type `α` such that `a R b`, then the quotients `a / r` and `b / r` are equal.
|
EqvGen.is_equivalence
theorem EqvGen.is_equivalence : ∀ {α : Type u} (r : α → α → Prop), Equivalence (EqvGen r)
This theorem states that for any type `α` and any binary relation `r` on `α`, the equivalence closure of `r` (denoted by `EqvGen r`) is an equivalence relation. In other words, for any given relation `r` on elements of a certain type, the relation that includes `r` and the smallest possible amount of additional pairs to make it reflexive, symmetric and transitive, is indeed an equivalence relation.
More concisely: For any binary relation `r` on type `α`, the reflexive, symmetric, and transitive closure of `r` (denoted by `EqvGen r`) equals the equivalence relation on `α` induced by `r`.
|