PEquiv.injective_of_forall_ne_isSome
theorem PEquiv.injective_of_forall_ne_isSome :
∀ {α : Type u} {β : Type v} (f : α ≃. β) (a₂ : α),
(∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true) → Function.Injective ⇑f
This theorem states that for any type `α` and `β`, given a partial equivalence `f` between `α` and `β`, and an element `a₂` from `α`, if for every other element `a₁` from `α` that is not equal to `a₂` the partial function `f` is defined, then the function `f` is injective. In other words, if `f` is defined for all elements in the domain `α` except possibly for a single point `a2`, then no two distinct elements of `α` map to the same element of `β` under `f`.
More concisely: If `f` is a partial equivalence from type `α` to type `β` such that for all `a₁ ≠ a₂` in `α`, `f` is defined, then `f` is injective.
|
Mathlib.Data.PEquiv._auxLemma.5
theorem Mathlib.Data.PEquiv._auxLemma.5 : ∀ {α : Type u_1} {a : α} {b : Option α}, (a ∈ b) = (b = some a)
This theorem, `Mathlib.Data.PEquiv._auxLemma.5`, asserts that for any type `α` and any element `a` of that type, as well as any `Option` of `α` named `b`, the statement "a is in b" is equivalent to the statement "b is equal to `some a`". In other words, an element `a` is contained in an `Option` `b` if and only if `b` is `some a` in the context of optional values in the type `α`.
More concisely: For any type `α` and `a : α`, the option `b : Option α` contains `a` if and only if `b` is `some a`.
|
PEquiv.injective_of_forall_isSome
theorem PEquiv.injective_of_forall_isSome :
∀ {α : Type u} {β : Type v} {f : α ≃. β}, (∀ (a : α), (f a).isSome = true) → Function.Injective ⇑f
The theorem states that if a partial equivalence `f` from type `α` to `β` has its domain covering all elements of `α` (i.e., for every element `a` of `α`, `f a` is defined), then the function in the forward direction, `⇑f`, is injective. In other words, if `f` is defined for all elements of `α`, then for any two elements `a₁` and `a₂` in `α`, if `⇑f(a₁)` equals `⇑f(a₂)`, it implies that `a₁` equals `a₂`.
More concisely: If a partial equivalence `f` from type `α` to `β` is total (i.e., defined for all elements of `α`), then `f` is injective (i.e., maps distinct elements to distinct images).
|
PEquiv.symm_injective
theorem PEquiv.symm_injective : ∀ {α : Type u} {β : Type v}, Function.Injective PEquiv.symm
The theorem `PEquiv.symm_injective` states that for any two types `α` and `β`, the function `PEquiv.symm`, which takes a partial equivalence from `α` to `β` and returns its inverse partial equivalence from `β` to `α`, is injective. In other words, if two partial equivalences from `α` to `β` have the same inverse partial equivalence, then they must have been the same partial equivalence to begin with.
More concisely: If two partial equivalences from type `α` to type `β` have the same inverse, then they are equal.
|
PEquiv.ext
theorem PEquiv.ext : ∀ {α : Type u} {β : Type v} {f g : α ≃. β}, (∀ (x : α), f x = g x) → f = g
This theorem, `PEquiv.ext`, states that for any two partial equivalences `f` and `g` between two types `α` and `β`, if for every element `x` of type `α`, `f` applied to `x` is equal to `g` applied to `x`, then `f` and `g` are indeed the same partial equivalence. In other words, two partial equivalences are identical if they yield the same result for every input from their domain.
More concisely: If two partial equivalences between types `α` and `β` agree on every element from their domain, then they are equal as partial equivalences.
|
Mathlib.Data.PEquiv._auxLemma.4
theorem Mathlib.Data.PEquiv._auxLemma.4 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, `Mathlib.Data.PEquiv._auxLemma.4`, asserts that for any type `α` and any two elements `a` and `b` of that type, the statement that `a` equals `b` is equivalent to the statement that `b` equals `a`. This is a fundamental property of equality, known as symmetry, which states that if `a` is equal to `b`, then `b` is also equal to `a`.
More concisely: For all types `α` and elements `a, b` of `α`, `a = b` if and only if `b = a`.
|
PEquiv.inv
theorem PEquiv.inv :
∀ {α : Type u} {β : Type v} (self : α ≃. β) (a : α) (b : β), a ∈ self.invFun b ↔ b ∈ self.toFun a
This theorem states that for any types `α` and `β`, and any partial equivalence `self` between them, an element `a` of type `α` is in the inverse function of `b` if and only if `b` is in the function of `a`. In other words, `invFun` and `toFun` are inverses of each other when applied to particular elements `a` and `b`.
More concisely: For any partial equivalences `self` between types `α` and `β`, `a ∈ self.invFun b` if and only if `b ∈ self.toFun a`.
|
PEquiv.eq_some_iff
theorem PEquiv.eq_some_iff :
∀ {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β}, f.symm b = some a ↔ f a = some b
This theorem states that for any partial equivalence `f` between two types `α` and `β`, and for any elements `a` of type `α` and `b` of type `β`, the partial equivalence `f` maps `a` to `some b` if and only if the inverse of `f` maps `b` to `some a`. In other words, an element `a` is in the domain of the partial function `f` with image `b` if and only if `b` is in the domain of the inverse partial function with image `a`.
More concisely: For any partial equivalence relation `R` on types `α` and `β`, `a ��:`α` R b ↔ b ∋ a. (Here, `∋` denotes the existence quantifier, and `∉` its negation, meaning "there exists" and "there does not exist" respectively.) In other words, `a` is related to `b` by `R` if and only if `b` is related to `a` by the inverse relation.
|