Semiquot.ext_s
theorem Semiquot.ext_s : ∀ {α : Type u_1} {q₁ q₂ : Semiquot α}, q₁ = q₂ ↔ q₁.s = q₂.s
This theorem states that for any type `α`, and any two objects `q₁` and `q₂` of type `Semiquot α`, `q₁` is equal to `q₂` if and only if the `.s` field of `q₁` is equal to the `.s` field of `q₂`. In other words, two semiquotients of the same type are equal exactly when their `.s` fields, which represent the underlying set, are equal.
More concisely: For any type `α` and semiquotients `q₁` and `q₂` of type `Semiquot α`, `q₁ = q₂` if and only if `q₁.s = q₂.s`.
|
Semiquot.ext
theorem Semiquot.ext : ∀ {α : Type u_1} {q₁ q₂ : Semiquot α}, q₁ = q₂ ↔ ∀ (a : α), a ∈ q₁ ↔ a ∈ q₂
The theorem `Semiquot.ext` states that for any type `α` and any two semiquotients `q₁` and `q₂` of that type, `q₁` is equal to `q₂` if and only if for any element `a` of type `α`, `a` is a member of `q₁` if and only if `a` is a member of `q₂`. In other words, two semiquotients are equal if they contain exactly the same elements.
More concisely: Two semiquotients of a type are equal if and only if they contain the same elements.
|
Mathlib.Data.Semiquot._auxLemma.6
theorem Mathlib.Data.Semiquot._auxLemma.6 : ∀ {α : Type u_1} {a b : α}, (a ∈ pure b) = (a = b)
This theorem, from the Mathlib library in Lean 4, states that for any type `α` and any two elements `a` and `b` of `α`, the proposition that `a` is in the set `pure b` is equivalent to the proposition that `a` equals `b`. Here, `pure` is a function from the underlying type to a type of sets over the underlying type. In the context of this theorem, `pure b` can be seen as a set that contains only the element `b`.
More concisely: For any type `α` and any two elements `a` and `b` of `α`, `a` is in the singleton set `{b}` (denoted `pure b`) if and only if `a` equals `b`.
|