Setoid.ext'
theorem Setoid.ext' : ∀ {α : Type u_1} {r s : Setoid α}, (∀ (a b : α), r.Rel a b ↔ s.Rel a b) → r = s
The theorem `Setoid.ext'` states that for any type `α` and any two Setoids `r` and `s` over that type, if the relation defined by `r` between any two elements of type `α` is equivalent to the relation defined by `s` between the same two elements, then the Setoids `r` and `s` are the same. Here, `Setoid.Rel r a b` represents the relation `r` between elements `a` and `b` of type `α`, and equivalence of relations is defined as logical equivalence (i.e., `r` and `s` are equivalent if for any `a` and `b`, `r` holds between `a` and `b` if and only if `s` holds between `a` and `b`).
More concisely: If for all `α` and elements `a, b` of type `α`, the relations `r` and `s` defined on `α` hold between `a` and `b` equivalently, then `r` and `s` are equal as Setoids over `α`.
|
Setoid.inf_def
theorem Setoid.inf_def : ∀ {α : Type u_1} {r s : Setoid α}, (r ⊓ s).Rel = r.Rel ⊓ s.Rel
The theorem `Setoid.inf_def` states that for any type `α` and any two equivalence relations `r` and `s` on `α`, the infimum (greatest lower bound) of `r` and `s` as setoid relations is the same as the infimum of `r` and `s` as underlying binary operations. In other words, the meet operation (infimum) on equivalence relations corresponds directly to the meet operation on their associated binary relations.
More concisely: For any type `α` and equivalence relations `r` and `s` on `α`, the infimum of `r` and `s` as setoid relations equals the infimum of `r` and `s` as binary operations.
|
Setoid.eqvGen_eq
theorem Setoid.eqvGen_eq :
∀ {α : Type u_1} (r : α → α → Prop), EqvGen.Setoid r = sInf {s | ∀ ⦃x y : α⦄, r x y → s.Rel x y}
The theorem `Setoid.eqvGen_eq` states that for any type `α` and a binary relation `r` on `α`, the inductively defined equivalence closure of `r` (which is `EqvGen.Setoid r`) is the greatest lower bound or infimum (`sInf`) of the set of all equivalence relations that contain `r`. In other words, it's the smallest equivalence relation that extends `r`. This equivalence relation is represented by the set `{s | ∀ ⦃x y : α⦄, r x y → Setoid.Rel s x y}`, meaning the set of all equivalence relations `s` such that if `r` holds between `x` and `y`, then `s` also holds between `x` and `y`.
More concisely: The `Setoid.eqvGen_eq` theorem in Lean 4 asserts that the equivalence closure of a binary relation `r` on type `α` is the smallest equivalence relation containing `r`.
|
Setoid.ker_mk_eq
theorem Setoid.ker_mk_eq : ∀ {α : Type u_1} (r : Setoid α), Setoid.ker Quotient.mk'' = r
The theorem `Setoid.ker_mk_eq` states that for any type `α` and any equivalence relation `r` on `α`, the kernel of the quotient map induced by `r` is exactly `r` itself. Here, the 'kernel' of a function refers to the equivalence relation under which two elements are deemed equivalent if, and only if, they are mapped to the same value by the function. In this case, the function is `Quotient.mk''`, which produces the quotient set under the given equivalence relation. Thus, the theorem essentially asserts that producing a quotient set under some equivalence relation and then considering the equivalence relation induced by the mapping to this quotient set gives back the original equivalence relation.
More concisely: For any type `α` and equivalence relation `r` on `α`, the kernel of the quotient map induced by `r` (i.e., the equivalence relation on `α` induced by the quotient map) is equal to the given equivalence relation `r`.
|
Setoid.sup_def
theorem Setoid.sup_def : ∀ {α : Type u_1} {r s : Setoid α}, r ⊔ s = EqvGen.Setoid (r.Rel ⊔ s.Rel)
This theorem states that for all types `α` and any two equivalence relations `r` and `s` on `α`, the supremum (or join) of `r` and `s` is equal to the equivalence closure of the supremum of the underlying binary operations of `r` and `s`. Here, the equivalence closure of a relation is the smallest equivalence relation that contains the relation, and the supremum of two relations is the relation that relates two elements if and only if at least one of the original relations does.
More concisely: For all types `α` and equivalence relations `r` and `s` on `α`, the supremum of `r` and `s` equals the equivalence relation generated by their combined reflexive, symmetric, and transitive closure. (Note: In Lean, the supremum of relations is defined as the transitive closure of their union.)
|
Setoid.eqvGen_idem
theorem Setoid.eqvGen_idem :
∀ {α : Type u_1} (r : α → α → Prop), EqvGen.Setoid (EqvGen.Setoid r).Rel = EqvGen.Setoid r
This theorem states that the process of taking the equivalence closure of a relation is idempotent. In other words, for any type `α` and any relation `r` on `α`, taking the equivalence closure of the equivalence closure of `r` (that is, `EqvGen.Setoid (EqvGen.Setoid r).Rel`) is the same as taking the equivalence closure of `r` once (that is, `EqvGen.Setoid r`). This means applying the operation of taking the equivalence closure twice does not change the result beyond the initial application.
More concisely: The operation of taking equivalence closures in Lean is idempotent, meaning applying it twice to a relation results in the same equivalence relation.
|
Setoid.trans'
theorem Setoid.trans' : ∀ {α : Type u_1} (r : Setoid α) {x y z : α}, r.Rel x y → r.Rel y z → r.Rel x z
This theorem states that for any given type `α` and an equivalence relation `r` on `α`, and for any three elements `x`, `y`, `z` of type `α`, if `x` is related to `y` by `r` and `y` is related to `z` by `r`, then `x` is also related to `z` by `r`. In other words, this theorem is asserting the transitivity property of the equivalence relation `r`.
More concisely: If `r` is an equivalence relation on type `α`, then for all `x`, `y`, `z` in `α`, if `x r y` and `y r z`, then `x r z`.
|
Setoid.symm'
theorem Setoid.symm' : ∀ {α : Type u_1} (r : Setoid α) {x y : α}, r.Rel x y → r.Rel y x
This theorem, `Setoid.symm'`, states that for all types `α`, for any equivalence relation `r` on `α`, and for all elements `x` and `y` of `α`, if `x` is related to `y` under `r`, then `y` is also related to `x` under `r`. In other words, the relation `r` is symmetric: if `x` and `y` are elements such that `x` is related to `y` according to `r`, then `y` is related to `x` according to `r`. This is a common property in mathematics and is required for an equivalence relation.
More concisely: For all types `α` and equivalence relations `r` on `α`, if `x` is related to `y` under `r`, then `y` is related to `x` under `r` (reflexivity and symmetry property of equivalence relations).
|
Setoid.comm'
theorem Setoid.comm' : ∀ {α : Type u_1} (s : Setoid α) {x y : α}, s.Rel x y ↔ s.Rel y x
This theorem states that for all types `α` and for any setoid `s` on `α`, and for any elements `x` and `y` of `α`, the relation `Setoid.Rel` is symmetric. In other words, if `x` is related to `y` under the equivalence relation defined by `s`, then `y` is also related to `x` under the same equivalence relation. This is a typical property of equivalence relations, which are reflexive, symmetric, and transitive by definition. In terms of mathematical notation, this theorem can be written as: ∀ `α`, `s`, `x`, `y`, `Setoid.Rel s x y` if and only if `Setoid.Rel s y x`.
More concisely: For any equivalence relation `s` on type `α`, the relation `Setoid.Rel s` is symmetric. That is, for all `x` and `y` in `α`, `Setoid.Rel s x y` if and only if `Setoid.Rel s y x`.
|
Setoid.ext_iff
theorem Setoid.ext_iff : ∀ {α : Type u_1} {r s : Setoid α}, r = s ↔ ∀ (a b : α), r.Rel a b ↔ s.Rel a b
This theorem states that for any type `α` and any two setoids `r` and `s` on this type, `r` equals `s` if and only if, for all pairs of elements `(a, b)` of type `α`, the relation `Setoid.Rel r a b` is equivalent to the relation `Setoid.Rel s a b`. In other words, two setoids are considered equal if they establish the same relationships between all pairs of elements in the set.
More concisely: Two setoids on a type are equal if and only if they establish the same equivalence relation between all pairs of elements from that type.
|
Setoid.sup_eq_eqvGen
theorem Setoid.sup_eq_eqvGen :
∀ {α : Type u_1} (r s : Setoid α), r ⊔ s = EqvGen.Setoid fun x y => r.Rel x y ∨ s.Rel x y
The theorem `Setoid.sup_eq_eqvGen` states that for any two equivalence relations `r` and `s` on a type `α`, the supremum of `r` and `s` is equal to the equivalence closure of the binary relation which relates `x` and `y` if `x` is related to `y` by either `r` or `s`. In other words, the largest equivalence relation that contains both `r` and `s` is exactly the equivalence closure of the relation formed by the union of `r` and `s`.
More concisely: The largest equivalence relation containing both `r` and `s` equals the equivalence closure of `r ∪ s`.
|
Setoid.refl'
theorem Setoid.refl' : ∀ {α : Type u_1} (r : Setoid α) (x : α), r.Rel x x
The theorem `Setoid.refl'` states that, for any type `α` and any equivalence relation `r` on `α`, `Setoid.Rel r` is reflexive. That is, for every element `x` of type `α`, `x` is related to itself under the equivalence relation `r`. In mathematical terms, for all `x` in `α`, we have `Setoid.Rel r x x`. This is a formal statement of the reflexivity property of equivalence relations.
More concisely: For any equivalence relation `r` on type `α`, `x ∉-x` implies `∃ y, r x y ∧ r y x` (or equivalently, `Setoid.Rel r x x`).
|
Setoid.eqvGen_le
theorem Setoid.eqvGen_le :
∀ {α : Type u_1} {r : α → α → Prop} {s : Setoid α}, (∀ (x y : α), r x y → s.Rel x y) → EqvGen.Setoid r ≤ s := by
sorry
This theorem states that for any type `α` and any binary relation `r` on `α`, if there is an equivalence relation `s` on `α` such that `r` is a subset of `s` (in other words, `r x y` implies `s.Rel x y` for all `x` and `y` in `α`), then the equivalence closure of `r` (denoted `EqvGen.Setoid r`) is also a subset of `s`. In other words, any equivalence relation that contains `r` must also contain the equivalence closure of `r`.
More concisely: If `r` is a binary relation on type `α` and `s` is an equivalence relation on `α` such that `r` is a subset of `s`, then `EqvGen.Setoid r` (the equivalence closure of `r`) is also a subset of `s`.
|
Setoid.eqvGen_mono
theorem Setoid.eqvGen_mono :
∀ {α : Type u_1} {r s : α → α → Prop}, (∀ (x y : α), r x y → s x y) → EqvGen.Setoid r ≤ EqvGen.Setoid s
The theorem `Setoid.eqvGen_mono` states that the equivalence closure operation of binary relations is monotone. More specifically, for any type `α` and any two binary relations `r` and `s` on `α`, if every pair of elements `x` and `y` in `α` that satisfies the relation `r` also satisfies the relation `s`, then the equivalence closure of `r` is a subset of the equivalence closure of `s`. In other words, if `r` is a subrelation of `s`, then the equivalence closure of `r` is also a subrelation of the equivalence closure of `s`.
More concisely: If relation `r` is a subrelation of relation `s`, then the equivalence closures of `r` and `s` have the same equivalence classes.
|
Setoid.ker_lift_injective
theorem Setoid.ker_lift_injective :
∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Injective (Quotient.lift f ⋯)
The theorem `Setoid.ker_lift_injective` states that for any types `α` and `β` and any function `f` from `α` to `β`, the so-called natural map from the quotient of `α` by the kernel of `f`, which is constructed using the function `Quotient.lift`, is injective. In mathematical terms, this means that if two elements of the quotient space have the same image under this natural map, then they are actually the same element in the quotient space.
More concisely: If `α` and `β` are types and `f : α → β` is a function, then the natural map from the quotient of `α` by the kernel of `f`, constructed using `Quotient.lift`, is an injection.
|
Setoid.sSup_def
theorem Setoid.sSup_def : ∀ {α : Type u_1} {s : Set (Setoid α)}, sSup s = EqvGen.Setoid (sSup (Setoid.Rel '' s)) := by
sorry
The theorem `Setoid.sSup_def` states that for any set `s` of equivalence relations on a type `α`, the supremum (greatest lower bound) of `s` is equal to the equivalence closure of the supremum of the set's image under the map to the underlying binary operation. In other words, the maximal equivalence relation that is less than or equal to all relations in `s` is obtained by taking the image of `s` under the binary operation, and then taking the equivalence closure of that. This equivalence closure process extends the relation to ensure it is an equivalence relation (i.e., it is reflexive, symmetric, and transitive).
More concisely: The supremum of a set of equivalence relations on a type is equal to the equivalence closure of their composite relation.
|
Setoid.injective_iff_ker_bot
theorem Setoid.injective_iff_ker_bot :
∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Injective f ↔ Setoid.ker f = ⊥
This theorem states that a function `f` from type `α` to type `β` is injective (meaning that different inputs produce different outputs) if and only if the kernel of this function is the bottom element of the complete lattice of equivalence relations on `α`. In other words, the function `f` is injective precisely when its kernel, which is itself an equivalence relation, is the smallest or "least" equivalence relation in the set of all possible equivalence relations on `α`.
More concisely: A function between types is injective if and only if its kernel, as an equivalence relation, is the bottom element in the lattice of equivalence relations on the domain type.
|
Setoid.sSup_eq_eqvGen
theorem Setoid.sSup_eq_eqvGen :
∀ {α : Type u_1} (S : Set (Setoid α)), sSup S = EqvGen.Setoid fun x y => ∃ r ∈ S, r.Rel x y
This theorem states that for every set `S` of equivalence relations on a type `α`, the supremum of `S` is equivalent to the equivalence closure of the binary relation "there exists an equivalence relation `r` in `S` that relates `x` and `y`". In other words, the largest equivalence relation that is no greater than every relation in the set `S` is the equivalence closure of the relation that identifies two elements if and only if there is some relation in `S` that does so.
More concisely: The supremum of a set `S` of equivalence relations on type `α` is equivalent to the equivalence closure of the relation that identifies elements related by some relation in `S`.
|
Quotient.eq_rel
theorem Quotient.eq_rel : ∀ {α : Type u_1} {r : Setoid α} {x y : α}, Quotient.mk' x = Quotient.mk' y ↔ r.Rel x y := by
sorry
The theorem `Quotient.eq_rel` asserts that for any type `α` and an equivalence relation `r` on `α`, and for any two elements `x` and `y` of type `α`, the quotient elements of `x` and `y` (created by the quotient map `Quotient.mk'`) are equal if and only if `x` and `y` are related under the equivalence relation `r`. This theorem essentially provides a way to relate the equality of quotient elements to the underlying equivalence relation, thereby facilitating the process of rewriting in proofs.
More concisely: For any type `α` and equivalence relation `r` on `α`, the quotient map from `α` to `α / r` preserves equality, that is, `Quotient.mk r x = Quotient.mk r y` if and only if `x r y`.
|
Setoid.lift_unique
theorem Setoid.lift_unique :
∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (H : r ≤ Setoid.ker f) (g : Quotient r → β),
f = g ∘ Quotient.mk'' → Quotient.lift f H = g
The theorem `Setoid.lift_unique` states the uniqueness part of the universal property for quotients of an arbitrary type. Given a type `α`, an equivalence relation `r` on `α`, a function `f` from `α` to another type `β` such that `r` is included in the kernel of `f`, and a function `g` from the quotient of `α` by `r` to `β`, if `f` is equal to the composition of `g` with the function `Quotient.mk''` that sends each element of `α` to its equivalence class in the quotient, then the function `Quotient.lift f H` that lifts `f` to the quotient equals `g`. This means that any function from the quotient that extends `f` in this way is unique.
More concisely: If `f : α → β` maps an equivalence relation `r` on `α` to its quotient and satisfies `r ⊆ ker f`, then any function `g : α / r → β` extending `f` is equal to `Quotient.lift f`.
|
Setoid.ker_eq_lift_of_injective
theorem Setoid.ker_eq_lift_of_injective :
∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} (f : α → β) (H : ∀ (x y : α), r.Rel x y → f x = f y),
Function.Injective (Quotient.lift f H) → Setoid.ker f = r
This theorem states that for a given function `f` mapping from type `α` to type `β`, the kernel of `f` is the unique equivalence relation on `α` under the condition that the function induced by `f` from the quotient of `α` by the equivalence relation to `β` is injective. In other words, if an equivalence relation `r` on `α` satisfies the condition that whenever `x` and `y` are related by `r`, `f(x)` equals `f(y)`, then the injectivity of the quotient map ensures that the kernel of `f` must be this equivalence relation `r`. Here, the kernel of a function is the equivalence relation that identifies two elements if they are mapped to the same value by the function.
More concisely: Given a function `f` from type `α` to type `β`, the kernel of `f` is the unique equivalence relation on `α` such that the quotient map induced by `f` is injective.
|
Setoid.eq_iff_rel_eq
theorem Setoid.eq_iff_rel_eq : ∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ = r₂ ↔ r₁.Rel = r₂.Rel
The theorem states that two equivalence relations are equal if and only if their underlying binary operations are equal. Here, an equivalence relation is a type of binary relation that partitions a set into a collection of disjoint sets, called equivalence classes. Each of these relations is defined on a type `α` and the binary operations (`Rel`) of these relations are compared for equality. In other words, for all `α` of any type and any two equivalence relations `r₁` and `r₂` on `α`, `r₁` and `r₂` are the same equivalence relation if and only if the binary operations that define them are the same.
More concisely: Two equivalence relations on a type `α` are equal if and only if their defining binary operations are equal.
|
Setoid.sInf_def
theorem Setoid.sInf_def : ∀ {α : Type u_1} {s : Set (Setoid α)}, (sInf s).Rel = sInf (Setoid.Rel '' s)
The theorem `Setoid.sInf_def` states that for any type `α` and any set `s` of equivalence relations on `α`, the binary operation underlying the infimum (greatest lower bound) of the set of equivalence relations is equal to the infimum of the image of the set under the map to their underlying binary operations. In other words, computing the infimum of a set of equivalence relations and then extracting the binary operation is the same as first mapping each equivalence relation in the set to its binary operation and then computing the infimum of these operations.
More concisely: The infimum of the set of binary operations corresponding to equivalence relations in a set is equal to the binary operation underlying the infimum of those equivalence relations.
|
Setoid.ker_iff_mem_preimage
theorem Setoid.ker_iff_mem_preimage :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α}, (Setoid.ker f).Rel x y ↔ x ∈ f ⁻¹' {f y}
The theorem `Setoid.ker_iff_mem_preimage` states that for any types `α` and `β`, and any function `f : α → β`, and any elements `x` and `y` of type `α`, an element `x` is related to an element `y` by the kernel (equivalence relation) of the function `f` if and only if `x` belongs to the preimage of `f(y)` under the function `f`. In other words, two elements are related by the kernel of a function if and only if applying the function to both elements gives the same result.
More concisely: The kernel of a function `f : α → β` relates elements `x` and `y` in type `α` if and only if `x` and `y` map to the same image under `f`, i.e., `x ∉-f.preimage (f x) ↔ x = y`.
|
Setoid.comap_eq
theorem Setoid.comap_eq :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {r : Setoid β}, Setoid.comap f r = Setoid.ker (Quotient.mk'' ∘ f) := by
sorry
The theorem `Setoid.comap_eq` states that for any function `f` from type `α` to type `β` and any equivalence relation `r` on type `β`, the equivalence relation on type `α` induced by `f` is the same as the kernel of the composition of the quotient map `Quotient.mk''` and `f`. This essentially means that the equivalence classes on `α` obtained through `f` and `r` are the same as those obtained by first applying `f` and then taking the quotient with respect to `r`.
More concisely: The theorem asserts that the function-induced equivalence relation on type `α` coincides with the kernel of the composition of `Quotient.mk''` and `f` for any function `f` from type `α` to type `β` and equivalence relation `r` on type `β`.
|
Setoid.mapOfSurjective_eq_map
theorem Setoid.mapOfSurjective_eq_map :
∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (h : Setoid.ker f ≤ r) (hf : Function.Surjective f),
r.map f = r.mapOfSurjective f h hf
The theorem `Setoid.mapOfSurjective_eq_map` states that for any types `α` and `β`, any setoid `r` on `α`, and any function `f` from `α` to `β`, if the kernel of `f` is a subset of `r` and `f` is surjective (i.e., every element of `β` is the image of some element of `α` under `f`), then the mapping of `r` by `f` is equal to the mapping of `r` under `f` with respect to a surjection. In essence, this theorem establishes that the map of an equivalence relation through a surjective function is unchanged if we take into account that the function is surjective.
More concisely: If `f: α → β` is a surjective function and the kernel of `f` is a subset of the setoid `r` on `α`, then the mapping of `r` by `f` equals the mapping of `r` under `f`.
|
Mathlib.Data.Setoid.Basic._auxLemma.2
theorem Mathlib.Data.Setoid.Basic._auxLemma.2 :
∀ {α : Type u_1} {r s : Setoid α}, (r ≤ s) = ∀ {x y : α}, r.Rel x y → s.Rel x y
This theorem states that for any types `α` and any two Setoids `r` and `s` on `α`, the statement that `r` is a subset of `s` (denoted by `r ≤ s`) is equivalent to the statement that for all `x` and `y` of type `α`, if `x` and `y` are related by the relation `r` (denoted by `Setoid.Rel r x y`), then `x` and `y` are also related by the relation `s` (denoted by `Setoid.Rel s x y`). In mathematical terms, this is stating that one equivalence relation is a subset of another if and only if every pair of elements that are equivalent under the first relation are also equivalent under the second relation.
More concisely: For any Setoids `r` and `s` on a type `α`, `r ≤ s` if and only if for all `x` and `y` of type `α`, `Setoid.Rel r x y` implies `Setoid.Rel s x y`.
|
Setoid.eqvGen_of_setoid
theorem Setoid.eqvGen_of_setoid : ∀ {α : Type u_1} (r : Setoid α), EqvGen.Setoid Setoid.r = r
This theorem states that for any equivalence relation `r` on a type `α`, the equivalence closure (obtained by applying `EqvGen.Setoid` to `Setoid.r`) of `r` is `r` itself. In other words, if `r` is an equivalence relation, the process of repeatedly applying equivalence relations to extend `r` (which is what `EqvGen.Setoid` does, effectively taking the "closure" of `r`) doesn't change `r`. Thus, `r` is already fully "closed" under the equivalence generation process.
More concisely: For any equivalence relation `r` on type `α`, the equivalence closure obtained by applying `EqvGen.Setoid` to `r` equals `r`.
|