Quotient.eq''
theorem Quotient.eq'' : ∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, Quotient.mk'' a = Quotient.mk'' b ↔ Setoid.r a b
The theorem `Quotient.eq''` states that for any sort `α` endowed with a setoid `s₁`, and for any two elements `a` and `b` of `α`, the quotient elements `Quotient.mk'' a` and `Quotient.mk'' b` are equal if and only if `a` and `b` are related by the distinguished equivalence relation `Setoid.r` of the setoid `s₁`. This theorem thereby provides a correspondence between equality in the quotient and the underlying equivalence relation in the original sort.
More concisely: For any setoid `s₁` on sort `α`, two elements `a` and `b` are equal in the quotient `Quotient.mk'' a` and `Quotient.mk'' b` if and only if they are related by the equivalence relation `Setoid.r` of `s₁`.
|
Quotient.out_eq
theorem Quotient.out_eq : ∀ {α : Sort u_1} [s : Setoid α] (q : Quotient s), ⟦q.out⟧ = q
The theorem `Quotient.out_eq` states that for any type `α` with an equivalence relation `s` (specified as a `Setoid α`), and for any quotient `q` of `s`, the equivalence class of the chosen element from `q` (obtained by applying `Quotient.out`) is equal to the original quotient `q`. In other words, it ensures that the element chosen from the equivalence class using the axiom of choice, when considered as an equivalence class again, gives back the original equivalence class.
More concisely: For any type `α` with an equivalence relation `s`, and quotient `q` of `s`, the element `Quotient.out q` is equal to the equivalence class `{x // s x q}` containing `q`.
|
surjective_quot_mk
theorem surjective_quot_mk : ∀ {α : Sort u_1} (r : α → α → Prop), Function.Surjective (Quot.mk r)
The theorem `surjective_quot_mk` states that for any type `α` and any relation `r` on `α`, the function `Quot.mk r`, which maps an element of `α` to its equivalence class under `r` in the quotient set, is surjective. In other words, for every equivalence class in the quotient set, there exists an element in `α` such that `Quot.mk r` of that element produces the given equivalence class.
More concisely: For any type `α` and relation `r` on `α`, the function `Quot.mk r` is a surjection from `α` to the quotient set by `r`.
|
Quotient.inductionOn₂'
theorem Quotient.inductionOn₂' :
∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁ → Quotient s₂ → Prop}
(q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
The theorem `Quotient.inductionOn₂'` in Lean 4 is a version of `Quotient.inductionOn₂` that takes `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments instead of instance arguments. Specifically, for any data types `α` and `β` with setoid relations `s₁` and `s₂`, respectively, and a proposition `p` that applies to elements of the quotient types `Quotient s₁` and `Quotient s₂`, if the proposition holds for any pairs of elements `a₁` in `α` and `a₂` in `β` (when these elements are considered as elements of the corresponding quotient types via `Quotient.mk''`), then the proposition also holds for any pair of elements `q₁` in `Quotient s₁` and `q₂` in `Quotient s₂`. This theorem is essentially a tool to help reason about quotient structures by reasoning about their equivalence classes.
More concisely: If `p` holds for all pairs of elements in the quotient types `Quotient s₁` and `Quotient s₂` obtained from sets with setoid relations `s₁` and `s₂`, respectively, then `p` holds for all pairs of quotient elements.
|
Quotient.exact'
theorem Quotient.exact' :
∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, Quotient.mk'' a = Quotient.mk'' b → Setoid.r a b
The theorem `Quotient.exact'` states that for any type `α` that has a `Setoid` relation `s₁`, and for any two elements `a` and `b` of `α`, if the quotient of `a` under the `Setoid` relation `s₁` is equal to the quotient of `b` under the same relation, then `a` and `b` are related by the equivalence relation for the `Setoid`, denoted `Setoid.r`. In other words, this theorem provides a way to retrieve the underlying relation from the equality of the quotient elements.
More concisely: For any setoid `s₁` on type `α`, if `a` and `b` have equal quotients under `s₁`, then `a` and `b` are related by the equivalence relation `Setoid.r` of `s₁`.
|
Quotient.ind'
theorem Quotient.ind' :
∀ {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁ → Prop},
(∀ (a : α), p (Quotient.mk'' a)) → ∀ (q : Quotient s₁), p q
The theorem `Quotient.ind'` states that for any type `α`, any setoid `s₁` on `α`, and any property `p` that might hold for elements of the quotient of `α` by `s₁`, if the property `p` holds for each element `a` of `α` when considered as an element of the quotient (i.e., `Quotient.mk'' a`), then the property `p` holds for any element `q` of the quotient. In other words, if you can prove something about every representative of an equivalence class, you can prove it about the entire class in the quotient set.
More concisely: Given a type `α`, a setoid `s₁` on `α`, and a property `p` such that `p` holds for `Quotient.mk '' a` for all `a` in `α`, then `p` holds for all elements of the quotient of `α` by `s₁`.
|
Quotient.surjective_Quotient_mk''
theorem Quotient.surjective_Quotient_mk'' : ∀ {α : Sort u_1} {s₁ : Setoid α}, Function.Surjective Quotient.mk'' := by
sorry
The theorem `Quotient.surjective_Quotient_mk''` states that the function `Quotient.mk''` is surjective. In other words, for any type `α` and setoid `s₁` on `α`, every element in the quotient type `Quotient s₁` is an image of some element from `α` under the function `Quotient.mk''`. That is, for every equivalence class in the quotient set, there exists an element from the original set that maps to that equivalence class using the function `Quotient.mk''`.
More concisely: For any setoid `s₁` on type `α`, the function `Quotient.mk''` maps every element in `Quotient s₁` to some element in `α`.
|
Quotient.inductionOn'
theorem Quotient.inductionOn' :
∀ {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁ → Prop} (q : Quotient s₁),
(∀ (a : α), p (Quotient.mk'' a)) → p q
The theorem `Quotient.inductionOn'` states that for any sort `α` and setoid `s₁` on `α`, any property `p` on the quotient of `s₁`, and any element `q` of the quotient, if the property `p` holds for all elements `a` of `α` when passed through the `Quotient.mk''` function, then the property `p` also holds for `q`. In other words, this theorem provides a principle of induction on elements of the quotient sort, where the property extends from representatives of equivalence classes to their corresponding equivalence classes in the quotient.
More concisely: If a property holds for all representatives of equivalence classes of a setoid on a sort, then it holds for any equivalence class in the quotient.
|
Trunc.exists_rep
theorem Trunc.exists_rep : ∀ {α : Sort u_1} (q : Trunc α), ∃ a, Trunc.mk a = q
This theorem, `Trunc.exists_rep`, states that for any type `α` and any element `q` of the type `Trunc α`, there exists an element `a` of type `α` such that `Trunc.mk a` is equal to `q`. In other words, every instance of the truncated type `Trunc α` has a representative value in the original type `α`.
More concisely: For every type `α` and every `q` in `Trunc α`, there exists an `a` in `α` such that `Trunc.mk a = q`.
|
Quotient.eq'
theorem Quotient.eq' : ∀ {α : Sort u_1} [s₁ : Setoid α] {a b : α}, Quotient.mk' a = Quotient.mk' b ↔ Setoid.r a b := by
sorry
The theorem `Quotient.eq'` states that for any type `α` with a given setoid structure `s₁`, and for any two elements `a` and `b` of type `α`, the canonical quotient map `Quotient.mk' a` equals `Quotient.mk' b` if and only if `a` and `b` are related by the equivalence relation `Setoid.r`. In other words, two elements `a` and `b` are sent to the same equivalence class in the quotient structure if and only if they are equivalent under the original setoid's equivalence relation.
More concisely: For any setoid `(α, s₁)` and elements `a` and `b` of type `α`, `Quotient.mk' a = Quotient.mk' b` if and only if `a s₁ b`.
|
Setoid.ext
theorem Setoid.ext : ∀ {α : Sort u_3} {s t : Setoid α}, (∀ (a b : α), Setoid.r a b ↔ Setoid.r a b) → s = t
The theorem `Setoid.ext` states that for any sort `α`, given two setoids `s` and `t` on `α`, if for every pair of elements `(a, b)` from `α`, the statement "a is related to b under setoid `s`" is equivalent to "a is related to b under setoid `t`" (i.e., `Setoid.r a b` is true under both setoids), then the two setoids `s` and `t` are identical. This theorem essentially provides a criterion for the equality of two setoids based on the equivalence of their respective relation conditions for all pairs of elements in the set.
More concisely: If two setoids on a sort have equivalent relation conditions for all pairs of elements, then they are equal.
|
Quotient.out_eq'
theorem Quotient.out_eq' : ∀ {α : Sort u_1} {s₁ : Setoid α} (q : Quotient s₁), Quotient.mk'' q.out' = q
The theorem `Quotient.out_eq'` states that for any sort `α` and any Setoid `s₁` on `α`, and for any quotient `q` of `s₁`, if you apply the function `Quotient.out'` to `q` to get an element of `α`, and then apply `Quotient.mk''` to that element, you will get back the original quotient `q`. Essentially, this theorem is saying that `Quotient.mk''` and `Quotient.out'` are inverse processes for any given quotient.
More concisely: For any quotient `q` of a Setoid `s` on sort `α`, `Quotient.mk'' (Quotient.out' q) = q`.
|
Quotient.sound'
theorem Quotient.sound' :
∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, Setoid.r a b → Quotient.mk'' a = Quotient.mk'' b
The theorem `Quotient.sound'` states that for any type `α` equipped with a `Setoid` structure `s₁` and for any two elements `a` and `b` of type `α`, if `a` and `b` are related by the equivalence relation defined by `Setoid.r`, then their quotient images under the function `Quotient.mk''` are equal. In other words, if two elements are equivalent in the setoid, their images in the quotient set are the same.
More concisely: For any Setoid `s₁` on type `α`, `Quotient.mk '' a = Quotient.mk '' b` holds if and only if `a` is related to `b` by the equivalence relation defined by `s₁`.
|
Quotient.eq
theorem Quotient.eq : ∀ {α : Sort u_1} [r : Setoid α] {x y : α}, ⟦x⟧ = ⟦y⟧ ↔ x ≈ y
This theorem, `Quotient.eq`, states that for any type `α` with a given setoid relation `r`, and any two elements `x` and `y` of type `α`, the equivalence class of `x` is equal to the equivalence class of `y` if and only if `x` is related to `y` by the setoid relation `r`. In other words, two elements are in the same equivalence class under a setoid relation if and only if they are related by that setoid relation.
More concisely: For any setoid type `α` and elements `x` and `y` of type `α`, their equivalence classes under the setoid relation `r` are equal if and only if `x` is related to `y` by `r`.
|
Quotient.ind₂'
theorem Quotient.ind₂' :
∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁ → Quotient s₂ → Prop},
(∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) →
∀ (q₁ : Quotient s₁) (q₂ : Quotient s₂), p q₁ q₂
The theorem `Quotient.ind₂'` states that for any two types `α` and `β` with setoids `s₁` and `s₂` respectively, and for any property `p` that relates an element of the quotient of `s₁` and an element of the quotient of `s₂`, if this property holds for all pairs of representatives `a₁` from `α` and `a₂` from `β` (where the representatives are converted to their respective quotient elements using `Quotient.mk''`), then the property holds for all elements in the respective quotient sets. In other words, it allows you to prove properties about elements of quotient sets by proving them about representative elements from the original sets.
More concisely: If a property `p` holds for the representative pairs `(a₁, a₂)` of elements `[a₁ : α]` and `[a₂ : β]` in setoids `s₁` and `s₂`, then `p` holds for their respective quotient elements in `s₁ /= s₂`.
|
Quotient.mk_out
theorem Quotient.mk_out : ∀ {α : Sort u_1} [inst : Setoid α] (a : α), ⟦a⟧.out ≈ a
The theorem `Quotient.mk_out` states that for any type `α` that is equipped with a setoid structure (an equivalence relation), and for any element `a` of `α`, when `a` is wrapped into an equivalence class using the `Quotient.mk` function (denoted as ⟦a⟧), and then one element is chosen from this equivalence class using the `Quotient.out` function, the chosen element is equivalent to the original element `a` under the equivalence relation of the setoid. In essence, it guarantees that when we pick out an element from an equivalence class, we always get something that is equivalent to the element we started with.
More concisely: For any setoid (equivalence relation) on type `α`, and for any `a` in `α`, `Quotient.out (Quotient.mk a) = a` holds under the equivalence relation.
|
Equivalence.quot_mk_eq_iff
theorem Equivalence.quot_mk_eq_iff :
∀ {α : Type u_3} {r : α → α → Prop}, Equivalence r → ∀ (x y : α), Quot.mk r x = Quot.mk r y ↔ r x y
The theorem `Equivalence.quot_mk_eq_iff` states that for any type `α` and any equivalence relation `r` on `α`, for any elements `x` and `y` of `α`, the quotient of `x` and `y` under relation `r` (i.e., `Quot.mk r x` and `Quot.mk r y`) are equal if and only if `x` and `y` are related by `r`. This essentially provides a characterization for when two elements are considered equivalent under the quotient construction, by linking it directly to the equivalence relation used to form the quotient.
More concisely: For any type `α` and equivalence relation `r` on `α`, `Quot.mk r x = Quot.mk r y` if and only if `x` is related to `y` by `r`.
|
Trunc.eq
theorem Trunc.eq : ∀ {α : Sort u_1} (a b : Trunc α), a = b
This theorem states that for any type `α`, and any two elements `a` and `b` of the type `Trunc α`, `a` is equal to `b`. Here, `Trunc α` is the quotient of `α` by the always-true relation, which effectively means that all elements in `Trunc α` are considered equal.
More concisely: For any type `α`, all elements in the quotient `Trunc α` defined as the type of equivalence classes under the relation `r := ∀ (x y : α), true` are equal.
|
Quot.out_eq
theorem Quot.out_eq : ∀ {α : Sort u_1} {r : α → α → Prop} (q : Quot r), Quot.mk r q.out = q
The theorem `Quot.out_eq` states that for any equivalence class `q` over a sort `α` with an equivalence relation `r`, if we choose an element from `q` using the function `Quot.out` and then form a new equivalence class with that chosen element, we get back the original equivalence class `q`. This demonstrates the consistency of the `Quot.out` function with the equivalence class structure.
More concisely: For any equivalence class `q` and its representative `x` in type `α` with respect to an equivalence relation `r`, `Quot.out (Quot.mk _ x) = q`.
|
Quotient.inductionOn₃'
theorem Quotient.inductionOn₃' :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ}
{p : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃),
(∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)) → p q₁ q₂ q₃
The theorem `Quotient.inductionOn₃'` provides a mechanism for proving properties about three elements of Quotient sets. Given setoids `s₁` for type `α`, `s₂` for `β`, and `s₃` for `γ`, and a property `p` that applies to elements of the Quotient sets of `s₁`, `s₂`, and `s₃`, it says that if this property holds for any representants `a₁`, `a₂`, and `a₃` of the equivalence classes (that is, `p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)`), then it will also hold for any elements `q₁`, `q₂`, `q₃` of the Quotient sets themselves (that is, `p q₁ q₂ q₃`). This allows us to reason about elements of Quotient sets by instead reasoning about elements of the original sets from which the Quotients are derived.
More concisely: Given setoids s₁, s₂, and s₃, and a property p that is preserved under the Quotient.mk'' function, if p holds for any representants of the equivalence classes in s₁, s₂, and s₃, then p holds for any elements in the corresponding Quotient sets.
|
Trunc.induction_on
theorem Trunc.induction_on : ∀ {α : Sort u_1} {β : Trunc α → Prop} (q : Trunc α), (∀ (a : α), β (Trunc.mk a)) → β q
The theorem `Trunc.induction_on` is a principle of induction for the `Trunc` type. For every type `α` and every property `β` that holds for every value of type `Trunc α`, if this property `β` holds for every value `a` of type `α` that has been wrapped in `Trunc.mk`, then this property `β` holds for every value `q` of type `Trunc α`. In other words, if we can show that a property holds for every possible pre-quotient value, then it holds for every value in the quotient type.
More concisely: If a property holds for all pre-quotients of type `Trunc α` and is closed under `Trunc.mk`, then it holds for all quotients of type `Trunc α`.
|
Quotient.lift_mk
theorem Quotient.lift_mk :
∀ {α : Sort u_1} {β : Sort u_2} [s : Setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α),
Quotient.lift f h ⟦x⟧ = f x
The theorem `Quotient.lift_mk` states that, for any types `α` and `β`, any setoid `s` on `α`, any function `f` from `α` to `β` that respects the equivalence relation `≈` of this setoid, and any element `x` of `α`, applying the `Quotient.lift` function to `f`, the proof `h` that `f` respects `≈`, and the equivalence class of `x` (denoted by `⟦x⟧`) is equal to the value of `f` at `x`. In other words, `f` can be "lifted" to a function on the quotient of `α` by `≈`, and this lifted function behaves the same way as `f` on the representatives of the equivalence classes.
More concisely: Given a setoid `s` on type `α`, a function `f` from `α` to `β` respecting `≈`, and an element `x` of `α`, `Quotient.lift f h (⟨x⟩s) = f x`, where `h` is the proof of `f` respecting `≈`.
|
Quotient.map'_mk''
theorem Quotient.map'_mk'' :
∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β) (h : (Setoid.r ⇒ Setoid.r) f f) (x : α),
Quotient.map' f h (Quotient.mk'' x) = Quotient.mk'' (f x)
The theorem `Quotient.map'_mk''` states that for any types `α` and `β`, equipped with the equivalence relations `s₁` and `s₂` respectively, and for any function `f` from `α` to `β` that preserves the equivalence relationships, applying `Quotient.map'` to the quotient of an element under `f` is the same as forming the quotient of the image of the element under `f`. In other words, if `f` is a function that sends equivalent elements in `α` to equivalent elements in `β`, then mapping `f` over the quotient of an element `x` in `α` gives the same result as taking the quotient of `f(x)` in `β`.
More concisely: For any functions `f` preserving equivalence relations `s₁` on `α` and `s₂` on `β`, Quotient.map' applied to `f` on the quotient of an element `x ∈ α` is equal to the quotient of `f(x)` in `β`.
|
Quotient.mk_out'
theorem Quotient.mk_out' : ∀ {α : Sort u_1} {s₁ : Setoid α} (a : α), Setoid.r (Quotient.mk'' a).out' a
This theorem states that for any type `α` with an associated Setoid structure `s₁`, and any element `a` of type `α`, the `Setoid.r` relation holds true between `a` and the result of applying `Quotient.out'` to the result of `Quotient.mk''` applied to `a`. Intuitively, this says that when we make a quotient of `a` (using `Quotient.mk''`) and then retrieve a representative from this quotient (using `Quotient.out'`), this representative is related to the original element `a` under the equivalence relation of the Setoid structure.
More concisely: For any type `α` with a Setoid structure `s₁`, and for any `a` in `α`, `Setoid.r a (Quotient.out' (Quotient.mk'' a))` holds true.
|
Quot.eq
theorem Quot.eq : ∀ {α : Type u_3} {r : α → α → Prop} {x y : α}, Quot.mk r x = Quot.mk r y ↔ EqvGen r x y
This theorem, `Quot.eq`, states that for any type `α` and a binary relation `r` on `α`, two quotients `Quot.mk r x` and `Quot.mk r y` are equal if and only if `x` and `y` generate the same equivalence relation under `r`. Equivalently, `x` and `y` are related by the smallest equivalence relation containing `r`. This theorem links the notion of equality in the quotient type to the underlying relation that defines the equivalence classes of the quotient type.
More concisely: For any type `α` and binary relation `r` on `α`, `Quot.mk r x = Quot.mk r y` if and only if `x` and `y` are equivalent under the smallest equivalence relation containing `r`.
|
Quot.induction_on
theorem Quot.induction_on :
∀ {α : Sort u_4} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r), (∀ (a : α), β (Quot.mk r a)) → β q
This theorem, `Quot.induction_on`, is a principle of mathematical induction for quotient types in Lean 4. For any type `α` and a binary relation `r` on `α`, and for any property `β` of the quotient type formed by `r` on `α`, if every element `a` of `α` satisfies the property `β` when considered as an element of the quotient type via the `Quot.mk` function, then every element `q` of the quotient type satisfies the property `β`. In other words, if we can prove that a property holds for all representatives of an equivalence class, then it holds for the whole equivalence class.
More concisely: If a property holds for the representatives of every equivalence class of a quotient type formed by a binary relation on a type, then it holds for every element of the quotient type.
|
Quot.induction_on₂
theorem Quot.induction_on₂ :
∀ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} {δ : Quot r → Quot s → Prop} (q₁ : Quot r)
(q₂ : Quot s), (∀ (a : α) (b : β), δ (Quot.mk r a) (Quot.mk s b)) → δ q₁ q₂
The theorem `Quot.induction_on₂` in Lean 4 is a principle of induction for double quotients. It states that for any sort `α` and `β`, and any two relations `r` on `α` and `s` on `β`, together with a property `δ` on the quotients `Quot r` and `Quot s`, if the property is proven for the representatives `Quot.mk r a` and `Quot.mk s b` for any `a` in `α` and `b` in `β`, then that property holds for any elements `q₁` in `Quot r` and `q₂` in `Quot s`.
More concisely: Given relations `r` on sort `α` and `s` on sort `β`, if property `δ` holds for all quotients `[a]≃\_r A` and `[b]≃\_s B`, then `δ` holds for all quotients `[a]` and `[b]` in `Quot r` and `Quot s`, respectively.
|
surjective_quotient_mk'
theorem surjective_quotient_mk' : ∀ (α : Sort u_3) [s : Setoid α], Function.Surjective Quotient.mk'
The theorem `surjective_quotient_mk'` states that for all types α equipped with a setoid relation, the canonical quotient map `Quotient.mk'` is a surjective function. In other words, for every element in the quotient set, there exists an element in the original set such that the quotient map applied to this element produces the given element in the quotient set. Surjectivity of `Quotient.mk'` ensures that every equivalence class in the quotient set can be generated by some element from the original set.
More concisely: For any setoid type α, the quotient map `Quotient.mk'` is a surjection from α to its quotient set.
|