Equiv.exists_congr_left
theorem Equiv.exists_congr_left :
∀ {α : Sort u_1} {β : Sort u_2} (f : α ≃ β) {p : α → Prop}, (∃ a, p a) ↔ ∃ b, p (f.symm b)
This theorem, `Equiv.exists_congr_left`, states that for all types `α` and `β`, given a bijective function `f` from `α` to `β`, and a property `p` on `α`, there exists an element of `α` that satisfies `p` if and only if there exists an element of `β` that, when transformed back to `α` through the inverse of `f`, satisfies `p`. In mathematical terms, this theorem asserts that the existential quantification of a property is preserved under a bijective (or equivalently invertible) mapping.
More concisely: For all types `α` and `β`, if `f` is a bijective function from `α` to `β` and `p` is a property on `α`, then there exists an `x ∈ α` with `p(x)` if and only if there exists a `y ∈ β` with `p(f⁻¹(y))`.
|
Equiv.coe_refl
theorem Equiv.coe_refl : ∀ {α : Sort u}, ⇑(Equiv.refl α) = id
This theorem states that for any type `α`, the function represented by the equivalence relation of `α` to itself (`Equiv.refl α`) is identical to the identity function. It emphasizes that applying the equivalency of a type to itself does not change any elements of that type, behaving just like the identity function.
More concisely: For any type `α`, the reflexivity relation of `Equiv.refl α` is equal to the identity function on `α`.
|
Equiv.self_trans_symm
theorem Equiv.self_trans_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans e.symm = Equiv.refl α
This theorem, `Equiv.self_trans_symm`, states that for all types `α` and `β`, if we have an equivalence `e` between `α` and `β`, then the composition of `e` and its inverse (i.e., `e.trans e.symm`) is equivalent to the identity mapping on `α` (i.e., `Equiv.refl α`). In other words, if you can transform `α` to `β` and then reverse it back to `α`, you essentially do nothing (you obtain the identity map), which is a fundamental property of all equivalences.
More concisely: For all types `α` and equivalences `e` between `α` and another type `β`, `e.trans e.symm = Equiv.refl α`.
|
Equiv.forall_congr_left'
theorem Equiv.forall_congr_left' :
∀ {α : Sort u} {β : Sort v} {p : α → Prop} (f : α ≃ β), (∀ (x : α), p x) ↔ ∀ (y : β), p (f.symm y)
This theorem states that, for any two types `α` and `β`, and for any property `p` applying to elements of `α`, if there is an equivalence `f` between `α` and `β`, then "for all `x` in `α`, `p x` holds" if and only if "for all `y` in `β`, `p (f.symm y)` holds". In other words, the truth of a property for all elements in one type is equivalent to the truth of the same property for all elements in the other type under the inverse of the equivalence function.
More concisely: For any equivalence between types `α` and `β` and property `p` on `α`, `∀ x ∈ α, p x ↔ ∀ y ∈ β, p (f.symm y)`, where `f` is the equivalence function.
|
Equiv.rightInverse_symm
theorem Equiv.rightInverse_symm : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.RightInverse ⇑f.symm ⇑f
The theorem `Equiv.rightInverse_symm` states that for any equivalence relation `f` between two types `α` and `β`, the function `f.symm` (the inverse of `f`) is a right inverse to `f`. In other words, if we apply `f` and then apply `f.symm` (i.e., we perform the composition `f ∘ f.symm`), we get the identity function on the type `β`. This is a property of all equivalence relations in Lean 4.
More concisely: For any equivalence relation `f` between types `α` and `β` in Lean 4, `f.symm` is a right inverse to `f`, i.e., `f ∘ f.symm = idβ`.
|
Equiv.coe_inj
theorem Equiv.coe_inj : ∀ {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β}, ⇑e₁ = ⇑e₂ ↔ e₁ = e₂
This theorem states that for any two types `α` and `β`, and any two equivalences `e₁` and `e₂` from `α` to `β`, the application of `e₁` equals the application of `e₂` if and only if `e₁` equals `e₂`. In simpler terms, it says that if two equivalences between the same pair of types have the same effect when applied, then these two equivalences are indeed the same.
More concisely: For any types `α` and `β` and equivalences `e₁` and `e₂` from `α` to `β`, `e₁ = e₂` if and only if `e₁ ∘ x = e₂ ∘ x` for all `x : α`.
|
Equiv.forall_congr
theorem Equiv.forall_congr :
∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (f : α ≃ β),
(∀ {x : α}, p x ↔ q (f x)) → ((∀ (x : α), p x) ↔ ∀ (y : β), q y)
This theorem, `Equiv.forall_congr`, states that for any types `α` and `β`, and any propositions `p` applicable to elements of `α` and `q` applicable to elements of `β`, given a bijective mapping `f` from `α` to `β`, if for all elements `x` of `α`, `p` holds for `x` if and only if `q` holds for `f(x)`, then the proposition `p` holds for all elements of `α` if and only if the proposition `q` holds for all elements of `β`. In other words, we can transport a universal condition across a bijective (equivalent) mapping between sets.
More concisely: Given a bijective function `f` between types `α` and `β`, if `p(x) ↔ q(f x)` for all `x` in `α`, then `∀x ∈ α, p x ↔ ∀x ∈ β, q x`.
|
Equiv.cast_eq_iff_heq
theorem Equiv.cast_eq_iff_heq : ∀ {α β : Sort u_1} (h : α = β) {a : α} {b : β}, (Equiv.cast h) a = b ↔ HEq a b := by
sorry
This theorem, `Equiv.cast_eq_iff_heq`, states that for any two types `α` and `β` in a universe `u_1`, given a proof `h` of their equality, and for any elements `a` of type `α` and `b` of type `β`, the application of the equivalence `Equiv.cast h` to `a` is equal to `b` if and only if `a` and `b` are heterogeneously equal, denoted as `HEq a b`. In other words, it relates the equality of types (`α = β`), their equivalence (`α ≃ β`) and heterogeneous equality of their elements.
More concisely: For any types `α` and `β` equal in a universe `u_1`, and for any `a : α` and `b : β`, `Equiv.cast (eq.refl a) = b` if and only if `a` and `b` are heterogeneously equal.
|
Equiv.forall_congr_left
theorem Equiv.forall_congr_left :
∀ {α : Sort u} {β : Sort v} {p : β → Prop} (f : α ≃ β), (∀ (x : α), p (f x)) ↔ ∀ (y : β), p y
This theorem states that, for all types `α` and `β`, and a property `p` defined for elements of `β`, given a bijective function `f` that maps from `α` to `β`, the property `p` holds for all elements `x` of type `α` under the function `f` if and only if `p` holds for all elements `y` of type `β`. In other words, if every element from `α` when transformed to `β` via `f` satisfies `p`, it is equivalent to all elements in `β` satisfying `p`.
More concisely: For any bijective function $f : \alpha \to \beta$ and property $p : \beta \to Prop$, $p(x) \iff p(f(x))$ for all $x : \alpha$.
|
Equiv.refl_apply
theorem Equiv.refl_apply : ∀ {α : Sort u} (x : α), (Equiv.refl α) x = x
This theorem states that for any type `α` and any element `x` of type `α`, applying the identity equivalence on `α` to `x` results in `x` itself. In other words, an identity function when applied to any element of its domain will always return the element itself. This identity function is manifested here as an "equivalence relationship", denoted by `Equiv.refl α`, which captures the concept of reflexivity in the context of type theory.
More concisely: For any type `α` and any of its elements `x`, `Equiv.refl α x` equals `x`.
|
Equiv.eq_symm_comp
theorem Equiv.eq_symm_comp :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β), f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
This theorem states that for all sorts or types `α`, `β`, and `γ`, and given an equivalence `e` between `α` and `β`, and functions `f` from `γ` to `α` and `g` from `γ` to `β`, `f` being equal to the composition of the inverse of `e` and `g` is equivalent to the composition of `e` and `f` being equal to `g`. In simpler terms, it expresses a property of function composition concerning inverse functions under the condition of type equivalence.
More concisely: For all types `α`, `β`, `γ`, functions `f : γ → α`, `g : γ → β`, and equivalence `e : α ≃ β`, `f = g ?. e ∘ f` if and only if `e ∘ f = g`.
|
Equiv.trans_refl
theorem Equiv.trans_refl : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans (Equiv.refl β) = e
The theorem `Equiv.trans_refl` states that for any types `α` and `β`, and any equivalence `e` from `α` to `β`, the transitive operation of `e` with the reflexive equivalence of `β` (which is an equivalence relation from `β` to itself) is equivalent to `e`. In simpler terms, it shows that, in the context of equivalence relations, applying an equivalence after a reflexive (identity) equivalence does not change the original equivalence. This theorem formalizes one of the properties of equivalence relations: if something is equivalent to itself (reflexivity), that doesn't affect the transition from one thing to another (transitivity).
More concisely: For any equivalences `e` from type `α` to type `β`, `e ∘ rrefl β` is equivalent to `e`, where `rrefl β` is the reflexive equivalence relation on `β`.
|
Equiv.symm_comp_eq
theorem Equiv.symm_comp_eq :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β), ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
The theorem `Equiv.symm_comp_eq` states that for all types `α`, `β`, and `γ`, given an equivalence `e` between `α` and `β`, and functions `f` from `γ` to `α` and `g` from `γ` to `β`, the composition of the inverse of `e` and `g` is equal to `f` if and only if `g` is equal to the composition of `e` and `f`. This theorem essentially describes a property of function composition under equivalence transformations.
More concisely: For all types α, β, γ, equivalences e between α and β, and functions f: γ -> α and g: γ -> β, if e ∘ f = g then f ∘ e⁻¹ = g.
|
Equiv.Perm.coe_subsingleton
theorem Equiv.Perm.coe_subsingleton : ∀ {α : Type u_1} [inst : Subsingleton α] (e : Equiv.Perm α), ⇑e = id
This theorem states that for any type `α` which is a subsingleton (i.e., a type that has at most one element), any permutation (bijection) `e` of `α` is equal to the identity function. In mathematical terms, if a set has at most one element, any permutation of the set is equivalent to the identity map. This theorem cannot be a simplification lemma because it incorrectly matches when `synonym α` is semireducible, causing issues with constructs like `Multiplicative.ofAdd`.
More concisely: Any permutation of a subsingleton type is equal to the identity function.
|
Equiv.refl_symm
theorem Equiv.refl_symm : ∀ {α : Sort u}, (Equiv.refl α).symm = Equiv.refl α
The theorem `Equiv.refl_symm` states that for any type `α`, the symmetric (or inverse) of the identity equivalence on `α` (denoted by `Equiv.refl α`) is the same as the identity equivalence on `α` itself. In other words, the inverse of the identity function is the identity function itself for any given type.
More concisely: For any type α, the symmetric equivalence Equiv.refl α equals the identity equivalence on α.
|
Equiv.apply_symm_apply
theorem Equiv.apply_symm_apply : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β), e (e.symm x) = x
This theorem, `Equiv.apply_symm_apply`, states that for all types α and β, if there's an equivalence `e` between them, then for any value `x` of type β, applying `e` to the result of applying the inverse of `e` (`e.symm`) to `x` brings you back to `x`. In other words, `e` and `e.symm` are inverses of each other. This might be seen as a formal way of saying that you can 'undo' the application of `e` by applying `e.symm` - a key property of equivalences in mathematics and logic.
More concisely: For any equivalence `e` between types `α` and `β`, `e (x.symm) = x` for all `x` of type `β`.
|
Equiv.ext
theorem Equiv.ext : ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, (∀ (x : α), f x = g x) → f = g
This theorem, named `Equiv.ext`, states that for any two equivalences `f` and `g` between two arbitrary types `α` and `β`, if for all elements `x` of type `α` the result of applying `f` and `g` to `x` is the same, then `f` and `g` themselves are the same. In other words, if two equivalence functions behave identically on every input, they are equal.
More concisely: If two functions `f` and `g` between types `α` and `β` are equal as relations (i.e., for all `x` in `α`, `f x = g x`), then `f` and `g` are equal as functions.
|
Equiv.trans_apply
theorem Equiv.trans_apply :
∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : α), (f.trans g) a = g (f a)
This theorem states that for any sorts `α`, `β`, and `γ`, and for any equivalences `f` between `α` and `β`, and `g` between `β` and `γ`, and for any element `a` of `α`, the application of the composition of `f` and `g` to `a` is the same as the application of `g` to the image of `a` under `f`. In mathematical terms, this is saying that $(f \circ g)(a) = g(f(a))$, which is a fundamental property of function composition.
More concisely: For any equivalences f : α ↔ β and g : β ↔ γ, and any element a in α, (f ∘ g)(a) = g(f(a)).
|
Equiv.Perm.ext_iff
theorem Equiv.Perm.ext_iff : ∀ {α : Sort u} {σ τ : Equiv.Perm α}, σ = τ ↔ ∀ (x : α), σ x = τ x
The theorem `Equiv.Perm.ext_iff` states that for any type `α` and any two permutations `σ` and `τ` of `α`, `σ` is equal to `τ` if and only if they are equal at each element of `α`. In other words, two permutations are considered identical if they map every element of the type to the same element.
More concisely: Two permutations of type `α` are equal if and only if they map each element to the same image.
|
Equiv.refl_trans
theorem Equiv.refl_trans : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), (Equiv.refl α).trans e = e
This theorem, named `Equiv.refl_trans`, states that for all types `α` and `β`, if there exists an equivalence `e` between `α` and `β`, then the composition of the reflexive equivalence on `α` and `e` is just `e`. In other words, precomposing any equivalence `e : α ≃ β` with the identity equivalence on `α` doesn't change `e`. This mirrors the mathematical concept that composing a function with the identity function leaves the original function unchanged.
More concisely: For all types `α` and `β` and equivalences `e : α ≈ β`, the composition of reflexivity on `α` and `e` equals `e`. In symbols, `rfl α ∘ e = e`.
|
Equiv.comp_symm_eq
theorem Equiv.comp_symm_eq :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ), g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
This theorem states that for all types `α`, `β`, and `γ`, given an equivalence `e` between `α` and `β`, and functions `f` from `β` to `γ` and `g` from `α` to `γ`, the composition of `g` with the inverse of `e` is equal to `f` if and only if `g` is equal to the composition of `f` with `e`. In simpler terms, this theorem captures a property of function composition in the presence of an equivalence between the two original types.
More concisely: For all types `α`, `β`, and `γ`, given an equivalence `e` between `α` and `β`, functions `f: β → γ`, and `g: α → γ`, if `g = f ∘ e.symm`, then `f = g ∘ e`.
|
Equiv.eq_comp_symm
theorem Equiv.eq_comp_symm :
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ), f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
This theorem states that for any types `α`, `β`, and `γ`, and for any equivalence `e` between `α` and `β`, a function `f` from `β` to `γ`, and a function `g` from `α` to `γ`, the function `f` is equal to the function `g` composed with the inverse of `e` if and only if the function `f` composed with `e` is equal to `g`. This theorem expresses the property of how composing functions with an equivalence and its inverse works.
More concisely: For any equivalence $e:\alpha \cong \beta$, functions $f:\beta \to \gamma$, and $g:\alpha \to \gamma$, if $f \circ e = g$, then $f = g \circ e^{-1}$.
|
Equiv.leftInverse_symm
theorem Equiv.leftInverse_symm : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.LeftInverse ⇑f.symm ⇑f
The theorem `Equiv.leftInverse_symm` states that for any equivalence `f` between two types `α` and `β`, the inverse of `f` (denoted by `f.symm`) is a left inverse to `f`. In other words, for every element `x` of type `α`, applying `f` followed by `f.symm` returns the original element `x`. This means `f.symm ∘ f = id` for all `x` in `α`.
More concisely: For any equivalence relation `f` between types `α` and `β`, the inverse `f.symm` of `f` is a left inverse, i.e., `f.symm ∘ f = id` on `α`.
|
Equiv.nonempty_congr
theorem Equiv.nonempty_congr : ∀ {α : Sort u} {β : Sort v}, α ≃ β → (Nonempty α ↔ Nonempty β)
This theorem, `Equiv.nonempty_congr`, states that for any two sorts (essentially type classes in Lean) `α` and `β`, if `α` is equivalent to `β`, denoted by `α ≃ β`, then the statement "there exists an element in `α`" (represented by `Nonempty α`) is logically equivalent to the statement "there exists an element in `β`" (represented by `Nonempty β`). In other words, if `α` and `β` are equivalent sorts, then `α` is nonempty if and only if `β` is nonempty.
More concisely: If `α` is equivalent to `β`, then `Nonempty α` is logically equivalent to `Nonempty β`.
|
Equiv.subsingleton
theorem Equiv.subsingleton : ∀ {α : Sort u} {β : Sort v}, α ≃ β → ∀ [inst : Subsingleton β], Subsingleton α
This theorem states that, for any types `α` and `β`, if `α` is equivalent to `β` and `β` is a subsingleton (meaning it contains at most one element), then `α` is also a subsingleton. In mathematical terms, it says that the property of being a subsingleton is preserved under equivalence of types.
More concisely: If `α` is equivalent to a subsingleton `β`, then `α` is a subsingleton.
|
Equiv.nonempty
theorem Equiv.nonempty : ∀ {α : Sort u} {β : Sort v}, α ≃ β → ∀ [inst : Nonempty β], Nonempty α
This theorem states that for any two types `α` and `β`, if there is an equivalence between `α` and `β`, and `β` is nonempty (i.e., there exists at least one value of type `β`), then `α` is also nonempty. In other words, if we can map every element of type `α` to some element of type `β`, and we know that there is at least one value of type `β`, then there must be at least one value of type `α`.
More concisely: If there exists an equivalence between types `α` and `β` and `β` is nonempty, then `α` is nonempty.
|
Equiv.apply_eq_iff_eq
theorem Equiv.apply_eq_iff_eq : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α}, f x = f y ↔ x = y
This theorem states that for any two elements `x` and `y` of some type `α`, and a given equivalence `f` between type `α` and some other type `β`, the equality of `f(x)` and `f(y)` (i.e., the images of `x` and `y` under the equivalence `f`) is equivalent to the equality of `x` and `y` themselves. In other words, an equivalence preserves the equality of elements: if two elements are equal, their images under the equivalence are equal, and vice versa.
More concisely: For any equivalence relation `f` between types `α` and `β`, and for all `x` and `y` in `α`, `x = y` if and only if `f(x) = f(y)`.
|
Equiv.surjective
theorem Equiv.surjective : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Surjective ⇑e
The theorem `Equiv.surjective` states that for any given types `α` and `β`, if there is an equivalence `e` between `α` and `β`, then the function corresponding to this equivalence, denoted by `⇑e`, is surjective. In other words, for every element `b` of type `β`, there exists an element `a` in type `α` such that `⇑e a = b`. This theorem therefore establishes the surjectivity of any function derived from an equivalence between two types.
More concisely: If `e` is an equivalence between types `α` and `β`, then the function `⇑e` is surjective: for every `b` in `β`, there exists `a` in `α` such that `e a = b`.
|
Equiv.symm_trans_self
theorem Equiv.symm_trans_self : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.trans e = Equiv.refl β
The theorem `Equiv.symm_trans_self` states that for any two types `α` and `β`, given an equivalence `e` between `α` and `β`, the composition of the inverse of `e` with `e` itself results in the identity equivalence on `β`. In other words, if we have a way to transform `α` to `β` and then transform it back from `β` to `α`, applying these transformations in sequence is the same as doing nothing. This reflects a fundamental property of equivalence, specifically the property of 'symmetric transitivity'.
More concisely: For any equivalence relation `e` on types `α` and `β`, the composition of `e.symm` (the symmetric relation) with `e` is equal to the identity relation on `β`.
|
Equiv.coe_fn_injective
theorem Equiv.coe_fn_injective : ∀ {α : Sort u} {β : Sort v}, Function.Injective fun e => ⇑e
The theorem `Equiv.coe_fn_injective` asserts that for any sorts `α` and `β`, the function that maps an equivalence `e : α ≃ β` to its corresponding function `⇑e : α → β` is injective. In other words, if two equivalences between `α` and `β` induce the same function from `α` to `β`, then the two equivalences were in fact the same.
More concisely: If two functions `e1, e2 : α → β` are equal, then the corresponding equivalences `e1 : α ≃ β` and `e2 : α ≃ β` are equal.
|
Equiv.symm_comp_self
theorem Equiv.symm_comp_self : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ⇑e.symm ∘ ⇑e = id
This theorem states that for any two types `α` and `β` and for any equivalence relation `e` between them, the composition of the inverse of `e` (`e.symm`) and `e` itself is the identity function. In other words, applying `e` and then its inverse `e.symm` to any element results in the original element. This is a formal statement of the property that an operation followed by its inverse results in no change, which is a fundamental property of all inverse operations.
More concisely: For any equivalence relation `e` on types `α` and `β`, `e.symm ∘ e = id`.
|
Equiv.self_comp_symm
theorem Equiv.self_comp_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ⇑e ∘ ⇑e.symm = id
This theorem states that for any types `α` and `β`, and for any equivalence `e` between `α` and `β`, the composition of `e` and its inverse (i.e., `e.symm`) is equivalent to the identity function. In mathematical terms, given any equivalence `e : α ≃ β`, applying `e` and then its inverse will yield the original element, exactly as if the identity function had been applied. This is a restatement of one of the fundamental properties of bijective (invertible) functions.
More concisely: For any equivalence `e : α ≃ β`, `e * e.symm` is equal to the identity function `id : α → α` (or `id : β → β`).
|
Equiv.bijective
theorem Equiv.bijective : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Bijective ⇑e
The theorem `Equiv.bijective` states that for any two types `α` and `β`, if there exists a bijective mapping `e` from `α` to `β` (denoted as `α ≃ β`), then the function denoted by `⇑e` (which refers to the application of `e`) is bijective. In other words, if there exists an equivalence between two types, then the function that represents this equivalence is both injective (no two different inputs give the same output) and surjective (every possible output is produced by some input).
More concisely: If `α ≃ β` (there exists a bijective function from `α` to `β`), then the application function `⇑e` is a bijective function from `α` to `β`.
|
Equiv.symm_apply_apply
theorem Equiv.symm_apply_apply : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), e.symm (e x) = x
This theorem states that for all types α and β, if there exists an equivalence between α and β (denoted as "e : α ≃ β"), then applying the equivalence to an element of α (denoted as "x : α") and then applying the inverse of the equivalence (denoted as "e.symm") to the result, we get back the original element. In simpler terms, this theorem supports the idea that the inverse of an equivalence undoes the effect of the original equivalence.
More concisely: For all types α and β and equivalences e : α ≃ β, for all x : α, e.symm (e x) = x.
|
Equiv.subsingleton_congr
theorem Equiv.subsingleton_congr : ∀ {α : Sort u} {β : Sort v}, α ≃ β → (Subsingleton α ↔ Subsingleton β)
This theorem states that for any sorts `α` and `β`, if `α` is equivalent to `β`, then `α` is a subsingleton if and only if `β` is a subsingleton. Here, a subsingleton is a type that has at most one element. In other words, if we can establish an equivalence between two sorts, then they either both have at most one element, or neither does.
More concisely: For any sorts `α` and `β`, if `α` is equivalent to `β`, then `α` is a subsingleton if and only if `β` is a subsingleton. (Equivalently, `α` and `β` have the same subsingleton property.)
|
Equiv.apply_eq_iff_eq_symm_apply
theorem Equiv.apply_eq_iff_eq_symm_apply :
∀ {α : Sort u} {β : Sort v} {x : α} {y : β} (f : α ≃ β), f x = y ↔ x = f.symm y
This theorem states that for any two types `α` and `β`, and any elements `x` of `α` and `y` of `β`, and a given equivalence `f` between `α` and `β`, the condition of `f x` being equal to `y` is equivalent to `x` being equal to the inverse of `f` applied to `y`. In mathematical terms, it is saying that if we have a bijective function `f`, then `f(x) = y` if and only if `x = f⁻¹(y)`. This is a common property in mathematics related to bijective (or invertible) functions.
More concisely: For any bijective function $f$ between types $\alpha$ and $\beta$, $f(x) = y$ if and only if $x = f^{-1}(y)$.
|
Equiv.injective
theorem Equiv.injective : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Injective ⇑e
The theorem `Equiv.injective` states that for all types `α` and `β`, if there exists a bijective function `e` from `α` to `β` (denoted as `α ≃ β`), then the function `e` is injective. In other words, for every two elements `a₁` and `a₂` in `α`, if `e` of `a₁` equals `e` of `a₂`, it implies that `a₁` equals `a₂`. This is the defining property of an injective function.
More concisely: If `α` and `β` are types with a bijective function `e : α ≃ β`, then `e` is injective (i.e., for all `a₁ a₂ : α`, if `e a₁ = e a₂`, then `a₁ = a₂`).
|
Equiv.right_inv'
theorem Equiv.right_inv' : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.RightInverse ⇑e.symm ⇑e
The theorem `Equiv.right_inv'` states that for any type equivalence `e` between two arbitrary types `α` and `β`, the function `e.symm` (which maps `β` to `α`) is a right inverse to the function `e` (which maps `α` to `β`). In other words, if you apply `e` to an element of `α` and then apply `e.symm`, you get the original element of `α` back. This is denoted as `f ∘ g = id`, where `f` is `e` and `g` is `e.symm`.
More concisely: For any type equivalence `e` between types `α` and `β`, `e.symm` is a right inverse to `e`, i.e., `e ∘ e.symm = id`.
|
Equiv.congr_fun
theorem Equiv.congr_fun : ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g → ∀ (x : α), f x = g x
The theorem `Equiv.congr_fun` states that for any two equivalent relations `f` and `g` between sorts `α` and `β`, if `f` equals `g`, then for any element `x` of type `α`, the application of `f` to `x` is equal to the application of `g` to `x`. In other words, it asserts that if two equivalence relations are the same, then their action on any element of the source sort is also the same.
More concisely: For any equivalence relations `f` and `g` between sorts `α` and `β`, if `f = g`, then `f x = g x` for all `x : α`.
|
Equiv.eq_symm_apply
theorem Equiv.eq_symm_apply : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α}, y = e.symm x ↔ e y = x := by
sorry
This theorem states that for any types `α` and `β`, for any equivalence relation `e` between `α` and `β`, and for any elements `x` in `β` and `y` in `α`, `y` is equal to the inverse of `e` applied to `x` if and only if `e` applied to `y` is equal to `x`. In other words, it connects the application of an equivalence relation and its inverse, and their relationships with the respective elements of the types.
More concisely: For any equivalence relation e on types α and β, x ∈ β, and y ∈ α, x = e. inverse(y) if and only if e(y) = x.
|
Equiv.Perm.ext
theorem Equiv.Perm.ext : ∀ {α : Sort u} {σ τ : Equiv.Perm α}, (∀ (x : α), σ x = τ x) → σ = τ
The theorem `Equiv.Perm.ext` states that for any types `α`, and for any two permutations `σ` and `τ` of `α`, if for all elements `x` of `α`, the application of `σ` to `x` equals the application of `τ` to `x`, then `σ` and `τ` are identical. In other words, two permutations are considered the same if they produce the same outcome on every element of the set.
More concisely: If two permutations of a set map every element to the same image, then they are equal.
|
Equiv.symm_symm
theorem Equiv.symm_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.symm = e
This theorem states that for any equivalence relation 'e' between two sorts (or types) 'α' and 'β', taking the symmetric of the symmetric of 'e' returns 'e'. In other words, the double application of the 'symm' operation to an equivalence 'e' is an identity operation, leaving 'e' unchanged. The 'symm' operation here refers to swapping the domain and codomain of the equivalence relation.
More concisely: For any equivalence relation e between types α and β, (symm e) ^^ (symm e) = e.
|
Equiv.toFun_as_coe
theorem Equiv.toFun_as_coe : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ⇑e
The theorem `Equiv.toFun_as_coe` states that for any two types `α` and `β` and a given equivalence `e` between them, the function `e.toFun` is the same as the coercion function `⇑e`. In other words, we can use the coercion function `⇑e` as a shorthand to represent the function `e.toFun` that converts elements of type `α` to elements of type `β` under the equivalence `e`. This theorem provides a convenient and succinct way to use equivalence functions in Lean 4.
More concisely: For any equivalence `e` between types `α` and `β`, the function `e.toFun` is equal to the coercion function `⇑e`.
|
Equiv.symm_apply_eq
theorem Equiv.symm_apply_eq : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α}, e.symm x = y ↔ x = e y := by
sorry
This theorem, "Equiv.symm_apply_eq", states that for any two types `α` and `β` and any equivalence `e` between these types, for all `x` of type `β` and `y` of type `α`, the inverse of `e` applied to `x` is equal to `y` if and only if `x` is equal to `e` applied to `y`. In simpler terms, if you have an equivalence between two types, you can apply the equivalence to a value and then apply the inverse equivalence to get back the original value, and vice versa.
More concisely: For any equivalence relation `e` on types `α` and `β`, `e(x) = y` if and only if `x = e⁻¹(y)`.
|