PartialEquiv.IsImage.compl
theorem PartialEquiv.IsImage.compl :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β}, e.IsImage s t → e.IsImage sᶜ tᶜ
The theorem `PartialEquiv.IsImage.compl` states that for any types `α` and `β`, any partial equivalence `e` from `α` to `β`, and any sets `s` of `α` and `t` of `β`, if `t` is an image of `s` under the partial equivalence `e`, then the complement of `t` is also an image of the complement of `s` under the same partial equivalence `e`. In other words, if we map `s` to `t` using `e`, then the elements not in `s` are mapped to the elements not in `t`.
In mathematical terms, it asserts that if $e$ maps $s$ to $t$, then $e$ also maps the set difference of $\alpha$ and $s$ (denoted $s^c$) to the set difference of $\beta$ and $t$ (denoted $t^c$).
More concisely: If $e$ is a partial equivalence from $\alpha$ to $\beta$ and $s \subseteq \alpha$ maps to $t \subseteq \beta$, then $e(s^c) = t^c$.
|
PartialEquiv.trans_source
theorem PartialEquiv.trans_source :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
(e.trans e').source = e.source ∩ ↑e ⁻¹' e'.source
The theorem `PartialEquiv.trans_source` states that for any three types `α`, `β`, and `γ`, and any two partial equivalences `e` from `α` to `β` and `e'` from `β` to `γ`, the source of the composite partial equivalence `PartialEquiv.trans e e'` is equal to the intersection of the source of `e` and the preimage of the source of `e'` under `e`. This means that the domain of the composed partial equivalence is the set of all elements in the domain of `e` for which the image under `e` also lies in the domain of `e'`.
More concisely: The source of the composite partial equivalence `PartialEquiv.trans e e'` is equal to the intersection of the source of `e` and the preimage of the source of `e'` under `e`. In other words, the domain of `PartialEquiv.trans e e'` is the subset of the domain of `e` where the image of `e` lies in the domain of `e'`.
|
PartialEquiv.IsImage.image_eq
theorem PartialEquiv.IsImage.image_eq :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.IsImage s t → ↑e '' (e.source ∩ s) = e.target ∩ t
The theorem `PartialEquiv.IsImage.image_eq` establishes that for any set `s` of type `α`, set `t` of type `β`, and a partial equivalence `e` between `α` and `β`, if `t` is an image of `s` under the partial equivalence `e`, then the image of the intersection of the source of `e` and `s` under `e` is equal to the intersection of the target of `e` and `t`. In more mathematical terms, if `t` is an image of `s` under `e`, then `e` maps `(e.source ∩ s)` directly onto `(e.target ∩ t)`.
More concisely: If `e` is a partial equivalence between sets `α` and `β`, `s ⊆ α`, and `t = e(s)`, then `e(source e ∩ s) = target e ∩ t`.
|
PartialEquiv.symm_mapsTo
theorem PartialEquiv.symm_mapsTo :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.MapsTo (↑e.symm) e.target e.source
This theorem states that for any partial equivalence `e` between types `α` and `β`, the function represented by the inverse of `e` maps the target set of `e` into its source set. In other words, if `e` is a partial equivalence from a subset of `α` to a subset of `β`, then the inverse of `e` will take any element in the targeted subset of `β` and map it back into the source subset of `α`.
More concisely: For any partial equivalence relation `e` between types `α` and `β`, the inverse of `e` maps the domain of `e` in `β` back to `α`.
|
Mathlib.Logic.Equiv.PartialEquiv._auxLemma.2
theorem Mathlib.Logic.Equiv.PartialEquiv._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α}, x ∈ e.source → (↑e x ∈ e.target) = True
This theorem from the `Mathlib.Logic.Equiv.PartialEquiv` module states that for any given partial equivalence `e` between two types `α` and `β`, if an element `x` of type `α` is in the source of `e`, then the result of applying `e` to `x`, denoted by `↑e x`, is in the target of `e`. This is always true. In other words, the partial equivalence `e` maps elements from its source to its target.
More concisely: If `e` is a partial equivalence between types `α` and `β`, then for all `x ∈ α`, `↑e x ∈ β`.
|
PartialEquiv.right_inv'
theorem PartialEquiv.right_inv' :
∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : β⦄, x ∈ self.target → ↑self (self.invFun x) = x := by
sorry
This theorem states that for any partial equivalence relation `PartialEquiv` between two types `α` and `β`, and for any value `x` of type `β` in the target set of this relation, applying the inverse function `invFun` to `x` and then applying the function `↑self` (which is the application of the relation to its argument) to the result, gives back the original value `x`. In other words, `invFun` serves as a right-inverse of the function `↑self` on the target set of the partial equivalence relation.
More concisely: For any partial equivalence relation `PartialEquiv` between types `α` and `β`, and for all `x` in the target set of the relation, `invFun (↑self x) = x`.
|
PartialEquiv.map_source
theorem PartialEquiv.map_source :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α}, x ∈ e.source → ↑e x ∈ e.target
This theorem states that for any given partial equivalence relation `e` between two types `α` and `β`, if an element `x` of type `α` belongs to the source set of the partial equivalence, then the image of `x` under the partial equivalence relation `e` belongs to the target set of `e`. In other words, the theorem ensures the well-definedness of the partial equivalence relation by confirming that the mapping of `x` is indeed within the target set of the partial equivalence relation.
More concisely: For any partial equivalence relation `e` between types `α` and `β`, if `x ∈ α` and `x ≈ᵥ e y` for some `y ∈ β`, then `y ∈ β`.
|
Mathlib.Logic.Equiv.PartialEquiv._auxLemma.7
theorem Mathlib.Logic.Equiv.PartialEquiv._auxLemma.7 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem states that for any type `α` and `β`, any function `f` from `α` to `β`, any set `s` of type `β`, and any element `a` of type `α`, the element `a` is in the preimage of the set `s` under the function `f` if and only if the image of `a` under `f` is in the set `s`. In mathematical terms, if we denote the preimage of a set `s` under a function `f` as `f⁻¹(s)`, then `a ∈ f⁻¹(s)` if and only if `f(a) ∈ s`.
More concisely: For any function `f` from type `α` to type `β`, and sets `s ∈ β`, the element `a ∈ α` belongs to the preimage `f⁻¹(s)` if and only if the image `f(a)` is in `s`.
|
PartialEquiv.EqOnSource.symm_eqOn
theorem PartialEquiv.EqOnSource.symm_eqOn :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → Set.EqOn (↑e.symm) (↑e'.symm) e.target := by
sorry
The theorem `PartialEquiv.EqOnSource.symm_eqOn` states that for any two types `α` and `β`, and any two partial equivalences `e` and `e'` between these types, if `e` and `e'` are equivalent, then the inverse functions of `e` and `e'` are equal on the target set of `e`. In other words, for all elements in the target set of `e`, the inverse of `e` applied to that element equals the inverse of `e'` applied to the same element.
More concisely: If `e` and `e'` are two equivalent partial equivalences between types `α` and `β`, then `e⁻¹` and `e'⁻¹` agree on the target set of `e`.
|
PartialEquiv.left_inv
theorem PartialEquiv.left_inv :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α}, x ∈ e.source → ↑e.symm (↑e x) = x
The theorem `PartialEquiv.left_inv` states that: for any two types `α` and `β`, and given a partial equivalence `e` from `α` to `β`, if an element `x` from the source set of `e` is taken, then applying the original partial equivalence `e` to `x` and then applying the inverse of the partial equivalence (i.e., `PartialEquiv.symm e`) to the result will return the original element `x`. This is a statement of the left-inverse property for the defined partial equivalence.
More concisely: For any partial equivalence \(e: \alpha \leftrightarrows \beta\), \(e \circ \text{PartialEquiv.symm } e = \text{id}_{\alpha}\).
|
PartialEquiv.IsImage.of_preimage_eq
theorem PartialEquiv.IsImage.of_preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.source ∩ ↑e ⁻¹' t = e.source ∩ s → e.IsImage s t
This theorem states that given types `α` and `β`, a partial equivalence `e` between `α` and `β`, and sets `s` of `α` and `t` of `β`, if the intersection of the source of `e` and the preimage of `t` under `e` is equal to the intersection of the source of `e` and `s`, then `e` is an image of `s` onto `t`. In other words, the set `s` is mapped to the set `t` under the partial equivalence `e`.
More concisely: If the source of a partial equivalence `e` intersects the preimage of `t` under `e` equally with the source intersecting `s`, then `t` is the image of `s` under `e`.
|
PartialEquiv.trans_assoc
theorem PartialEquiv.trans_assoc :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv β γ)
(e'' : PartialEquiv γ δ), (e.trans e').trans e'' = e.trans (e'.trans e'')
The theorem `PartialEquiv.trans_assoc` asserts the associativity of the operation `PartialEquiv.trans` across four arbitrary types `α`, `β`, `γ`, and `δ`. More specifically, for any three partial equivalences `e : PartialEquiv α β`, `e' : PartialEquiv β γ`, and `e'' : PartialEquiv γ δ`, the operation of composing these equivalences is associative. That is, first composing `e` and `e'`, and then composing the result with `e''`, yields the same result as first composing `e'` and `e''` and then composing `e` with the result.
More concisely: For any partial equivalences $e : \alpha \leftrightarrows \beta$, $e' : \beta \leftrightarrows \gamma$, and $e'' : \gamma \leftrightarrows \delta$, the composition $e' \circ e \circ e''$ is equal to $e \circ (e' \circ e'')$.
|
PartialEquiv.copy_eq
theorem PartialEquiv.copy_eq :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : α → β) (hf : ↑e = f) (g : β → α) (hg : ↑e.symm = g)
(s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t), e.copy f hf g hg s hs t ht = e
This theorem states that for any types `α` and `β`, a partial equivalence `e` from `α` to `β`, a function `f` from `α` to `β` which is equal to the forward function of `e`, a function `g` from `β` to `α` which is equal to the inverse function of `e`, and sets `s` and `t` of `α` and `β` respectively which are equal to the source and target of `e`, creating a copy of the partial equivalence `e` using `f`, `g`, `s`, and `t` produces the same partial equivalence `e`. In other words, copying a partial equivalence in this way results in an identical partial equivalence.
More concisely: For any partial equivalence `e` from `α` to `β`, its forward function `f`, inverse function `g`, source set `s`, and target set `t`, the copy of `e` created using `f`, `g`, `s`, and `t` is equal to `e`.
|
PartialEquiv.mem_symm_trans_source
theorem PartialEquiv.mem_symm_trans_source :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) {e' : PartialEquiv α γ} {x : α},
x ∈ e.source → x ∈ e'.source → ↑e x ∈ (e.symm.trans e').source
This theorem, named `PartialEquiv.mem_symm_trans_source`, is about partial equivalences (also known as partial bijections) in the context of differentiable manifolds. Specifically, it states that for any three types α, β, and γ, and given two partial equivalences `e` from α to β and `e'` from α to γ, if a value `x` from the type α is in the source of both `e` and `e'`, then the result of applying `e` to `x` (denoted as ↑e x) is in the source of the composition of the inverse of `e` and `e'` (denoted as `e.symm.trans e'`). This lemma can be particularly useful when `e` and `e'` are charts of a manifold.
More concisely: If `x` is in the domain of both partial equivalences `e` from `α` to `β` and `e'` from `α` to `γ`, then `↑e x` is in the domain of `e.symm.trans e'`.
|
PartialEquiv.EqOnSource.source_inter_preimage_eq
theorem PartialEquiv.EqOnSource.source_inter_preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β},
e ≈ e' → ∀ (s : Set β), e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
This theorem states that for any two types `α` and `β`, and any two partial equivalences `e` and `e'` between these types, if `e` is equivalent to `e'`, then for any set `s` of type `β`, the intersection of the source of `e` and the preimage of `s` under `e` is equal to the intersection of the source of `e'` and the preimage of `s` under `e'`. In other words, the preimage of a set under a partial equivalence preserves the intersection operation with the source of the equivalence when the equivalence itself is respected. This is an important property in the theory of partial equivalences and set theory.
More concisely: For any partial equivalences `e` and `e'` between types `α` and `β`, if `e` is equivalent to `e'`, then the intersections of their sources with the preimages of any set `s` under `e` and `e'`, respectively, are equal.
|
PartialEquiv.symm_trans_self
theorem PartialEquiv.symm_trans_self :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.trans e ≈ PartialEquiv.ofSet e.target
This theorem states that for any partial equivalence `e` between two types `α` and `β`, the composition of the inverse of `e` with `e` itself is equivalent to the identity function that is restricted only to the target set of `e`. In other words, if we first apply the inverse of `e` and then apply `e`, we essentially do nothing (i.e., perform the identity operation) for elements in the target of `e`.
More concisely: For any partial equivalence relation `e` between types `α` and `β`, `e.symm ∘ e = πr₂ at e.target`.
|
PartialEquiv.trans_source'
theorem PartialEquiv.trans_source' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
(e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
The theorem `PartialEquiv.trans_source'` states that for any three types `α`, `β`, and `γ`, and for any two partial equivalences `e` from `α` to `β` and `e'` from `β` to `γ`, the source of the partial equivalence obtained by composing `e` and `e'` is equal to the intersection of the source of `e` and the preimage under `e` of the intersection of the target of `e` and the source of `e'`. In mathematical terms, this states that if we have two partial equivalences `e : α ⇀ β` and `e' : β ⇀ γ`, the domain where their composition is defined is `e.source ∩ e⁻¹(e.target ∩ e'.source)`.
More concisely: The source of the partial equivalence obtained by composing `e` and `e'` is the intersection of `e.source` and the preimage of `e.target ∩ e'.source` under `e`.
|
PartialEquiv.map_source''
theorem PartialEquiv.map_source'' : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), ↑e '' e.source ⊆ e.target
This theorem, `PartialEquiv.map_source''`, states that for any partial equivalence relation `e` between two types `α` and `β`, the image of the `source` of `e` under `e` is a subset of the `target` of `e`. In other words, given a partial equivalence relation, if we take any element from its `source`, apply the relation to it (which may not be defined for some elements, hence the partiality), the resulting value will always be within the `target` set of the partial equivalence relation.
More concisely: For any partial equivalence relation e between types α and β, the image of the source of e under e is contained in the target of e. In symbols: ∀ x ∈ source e, ∃ y ∈ target e, e x y.
|
PartialEquiv.map_target
theorem PartialEquiv.map_target :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β}, x ∈ e.target → ↑e.symm x ∈ e.source
The theorem `PartialEquiv.map_target` states that for any types `α` and `β`, and any partial equivalence `e` from `α` to `β`, if an element `x` of type `β` is in the target set of `e`, then the image of `x` under the inverse of `e` (`PartialEquiv.symm e`) belongs to the source set of `e`. In other words, this theorem ensures that the inverse function of a partial equivalence correctly maps elements from its target set back to its source set.
More concisely: For any partial equivalence `e` from `α` to `β`, if `x ∈ β` is in the target set of `e`, then `e.symm.apply x ∈ α` belongs to the source set of `e`.
|
PartialEquiv.eq_of_eqOnSource_univ
theorem PartialEquiv.eq_of_eqOnSource_univ :
∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β),
e ≈ e' → e.source = Set.univ → e.target = Set.univ → e = e'
This theorem states that for any two partial equivalences `e` and `e'` between types `α` and `β`, if `e` and `e'` are equivalent, and both the source of `e` and the target of `e` are the universal set (meaning they contain all possible elements of their respective types), then `e` and `e'` must be equal. This emphasises the condition that the universality of the source and target, along with the equivalence of two partial equivalences, guarantees their equality.
More concisely: If two partial equivalences between universal types are equivalent, they are equal.
|
Mathlib.Logic.Equiv.PartialEquiv._auxLemma.5
theorem Mathlib.Logic.Equiv.PartialEquiv._auxLemma.5 :
∀ {α : Type u} {s t : Set α}, (s = t) = ∀ (x : α), x ∈ s ↔ x ∈ t
This theorem, from the Mathlib library in Lean 4, states that for any type `α`, and any two sets `s` and `t` of this type, the statement that `s` is equal to `t` is equivalent to the assertion that for every element `x` of type `α`, `x` is in `s` if and only if `x` is in `t`. In other words, two sets are equal if they contain exactly the same elements.
More concisely: For any type `α` and sets `s` and `t` of type `α`, `s = t` if and only if for all `x` in `α`, `x ∈ s` if and only if `x ∈ t`.
|
PartialEquiv.IsImage.leftInvOn_piecewise
theorem PartialEquiv.IsImage.leftInvOn_piecewise :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β}
[inst : (i : α) → Decidable (i ∈ s)] [inst_1 : (i : β) → Decidable (i ∈ t)],
e.IsImage s t →
e'.IsImage s t → Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)
This theorem, `PartialEquiv.IsImage.leftInvOn_piecewise`, states the property of the function `Set.piecewise` with respect to two partial equivalences and two sets. More specifically, given two types `α` and `β`, two partial equivalences `e` and `e'` from `α` to `β`, and two sets `s` of type `α` and `t` of type `β`, if `t` is an image of `s` under both `e` and `e'`, then the function `Set.piecewise t` applied to the inverse of `e` and the inverse of `e'` is a left inverse to `Set.piecewise s` applied to `e` and `e'` on the set that is the intersection of `s` with the source of `e` and the union of the complement of `s` with the source of `e'`. This property essentially captures the connection between the image of a set under a partial equivalence and the operation of piecewise-defined functions.
More concisely: Given sets `s` and `t`, partial equivalences `e` and `e'`, if `t` is the image of `s` under both `e` and `e'`, then `Set.piecewise t` applied to the inverses of `e` and `e'` is a left inverse to `Set.piecewise s` applied to `e` and `e'` on `s ∩ Dom e ∩ Dom e'` and `(Dom e \ s) ∪ (Dom e' \ s)`.
|
PartialEquiv.refl_trans
theorem PartialEquiv.refl_trans :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), (PartialEquiv.refl α).trans e = e
The theorem `PartialEquiv.refl_trans` states that for any two types `α` and `β` and any partial equivalence `e` between `α` and `β`, the composition of the identity partial equivalence on `α` and `e` is equal to `e`. Here, `PartialEquiv.trans` is a function that composes two partial equivalences, and `PartialEquiv.refl` is a function that returns the identity partial equivalence on a type. The identity partial equivalence is a partial equivalence that does not change any elements.
More concisely: For any types `α` and `β` and partial equivalence `e` between them, `PartialEquiv.refl α § e = e`, where `§` denotes composition of partial equivalences in Lean.
|
PartialEquiv.IsImage.symm_iff
theorem PartialEquiv.IsImage.symm_iff :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.symm.IsImage t s ↔ e.IsImage s t
This is a theorem about the notion of an image in the context of a partial equivalence between two sets. It states that for any types `α` and `β`, any partial equivalence `e` between `α` and `β`, and any sets `s` of `α` and `t` of `β`, the set `t` is an image of `s` under the inverse of `e` if and only if `s` is an image of `t` under `e`. This means that the concept of an image is preserved under the inversion of a partial equivalence.
More concisely: For any partial equivalences $e$ between types $\alpha$ and $\beta$, and sets $s \subseteq \alpha$ and $t \subseteq \beta$, $t$ is the image of $s$ under the inverse of $e$ if and only if $s$ is the image of $t$ under $e$.
|
PartialEquiv.transEquiv_eq_trans
theorem PartialEquiv.transEquiv_eq_trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : β ≃ γ),
e.transEquiv e' = e.trans e'.toPartialEquiv
The theorem `PartialEquiv.transEquiv_eq_trans` states that for all types `α`, `β`, and `γ`, and for a given partial equivalence `e` from `α` to `β` and an equivalence `e'` from `β` to `γ`, the composition of the partial equivalence `e` with the equivalence `e'` using `PartialEquiv.transEquiv` is equal to the composition of `e` with the conversion of `e'` to a partial equivalence using `PartialEquiv.trans` and `Equiv.toPartialEquiv`. In simpler terms, it ensures that the composition operation is consistent whether we consider `e'` as a full or partial equivalence.
More concisely: For all partial equivalences `e : α ≃_∞β` and equivalences `e' : β ≃ γ`, `PartialEquiv.transEquiv e e' = PartialEquiv.trans e (Equiv.toPartialEquiv e')`.
|
PartialEquiv.EqOnSource.trans'
theorem PartialEquiv.EqOnSource.trans' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e e' : PartialEquiv α β} {f f' : PartialEquiv β γ},
e ≈ e' → f ≈ f' → e.trans f ≈ e'.trans f'
This theorem states that the composition of partial equivalences respects equivalence. In particular, for any types `α`, `β`, and `γ`, and any partial equivalences `e`, `e'` between `α` and `β`, and `f`, `f'` between `β` and `γ`, if `e` is equivalent to `e'` and `f` is equivalent to `f'`, then the composition of `e` and `f` is equivalent to the composition of `e'` and `f'`. Here, `e.trans f` and `e'.trans f'` represent the compositions of the respective partial equivalences.
More concisely: If `e` is equivalent to `e'` and `f` is equivalent to `f'`, then `e.trans f` is equivalent to `e'.trans f'`. (where `e` and `e'` are partial equivalences between `α` and `β`, and `f` and `f'` are partial equivalences between `β` and `γ`)
|
PartialEquiv.EqOnSource.symm'
theorem PartialEquiv.EqOnSource.symm' :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → e.symm ≈ e'.symm
This theorem states that if two partial equivalences (from a type α to a type β) are equivalent, their inverses (from type β back to α) are also equivalent. In other words, the equivalence of two partial equivalences is preserved under the operation of taking the inverse.
More concisely: If two partial equivalences between types are equal, their inverses are also equal.
|
PartialEquiv.ext
theorem PartialEquiv.ext :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β},
(∀ (x : α), ↑e x = ↑e' x) → (∀ (x : β), ↑e.symm x = ↑e'.symm x) → e.source = e'.source → e = e'
The theorem `PartialEquiv.ext` states that for any two partial equivalences `e` and `e'` between two types `α` and `β`, if `e` and `e'` have the same source, and for every `x` in `α` and `β`, the application of `e` and `e'` (or their inverses) to `x` produces the same result, then `e` and `e'` must be identical. In other words, two partial equivalences are the same if they have the same source and map elements in the same way in both directions.
More concisely: If two partial equivalences between types have the same source and agree on their applications to elements, they are equal.
|
PartialEquiv.IsImage.iff_preimage_eq
theorem PartialEquiv.IsImage.iff_preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
The theorem `PartialEquiv.IsImage.iff_preimage_eq` states that for any types `α` and `β`, any partial equivalence `e` from `α` to `β`, and any sets `s` of `α` and `t` of `β`, the set `t` is an image of the set `s` under the partial equivalence `e` if and only if the intersection of the source of `e` and the preimage of `t` under `e` equals the intersection of the source of `e` and `s`. This provides a condition to check if a set is an image of another set under a partial equivalence.
More concisely: For any types α and β, partial equivalence e from α to β, and sets s of α and t of β, the sets s and the preimage of t under e have equal intersections with the source of e if and only if t is the image of s under e.
|
PartialEquiv.map_source'
theorem PartialEquiv.map_source' :
∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : α⦄, x ∈ self.source → ↑self x ∈ self.target := by
sorry
This theorem states that for any partial equivalence between two types `α` and `β`, if an element `x` belongs to the source set of the partial equivalence, then the image of `x` under the partial equivalence also belongs to the target set. This is a fundamental property of partial equivalences, ensuring that they correctly map elements from the source set to the target set.
More concisely: For any partial equivalence relation R on types α and β, if x ∈ α and ∃ y. x R y, then y ∈ β.
|
PartialEquiv.symm_source
theorem PartialEquiv.symm_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.source = e.target
The theorem `PartialEquiv.symm_source` states that for any partial equivalence `e` between two types `α` and `β`, the source of the inverse of `e` (denoted as `PartialEquiv.symm e`) is equivalent to the target of `e`. In other words, it reverses the roles of the source and target in the partial equivalence.
More concisely: For any partial equivalence `e` between types `α` and `β`, `PartialEquiv.symm e` is the partial equivalence with source `β` and target `α` such that `e (x : α) ≈ y : β <=> (x ≈ y) ≈ (y ≈ x)`.
|
PartialEquiv.IsImage.preimage_eq
theorem PartialEquiv.IsImage.preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.IsImage s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s
The theorem `PartialEquiv.IsImage.preimage_eq` states that for any two types `α` and `β`, a partial equivalence `e` from `α` to `β`, and two sets `s` of type `α` and `t` of type `β`, if `e` is an image of `s` on `t`, then the intersection of the source of `e` with the preimage of `t` under `e` is equal to the intersection of the source of `e` with `s`. In simpler terms, when `e` maps `s` onto `t`, the elements in the source of `e` that get mapped to `t` are exactly those in `s`.
More concisely: If `e` is a partial equivalence from `α` to `β` and `s ⊆ α` maps to `t ⊆ β` under `e`, then `s ∩ e⁁⁻¹(t) = e⁁⁻¹(t) ∩ α`.
|
PartialEquiv.IsImage.symm_preimage_eq
theorem PartialEquiv.IsImage.symm_preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
The theorem `PartialEquiv.IsImage.symm_preimage_eq` states that for any types `α` and `β`, any partial equivalence `e` between `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, if `e` images `s` to `t` (`e.IsImage s t`), then the intersection of the target of `e` with the preimage of `s` under the inverse of `e` is equal to the intersection of the target of `e` with `t`. In other words, the target elements of `e` that map back to `s` are exactly the ones that were originally mapped from `s` to `t` by `e`.
More concisely: For any partial equivalence `e` between types `α` and `β` and sets `s ⊆ α` and `t ⊆ β` such that `e.IsImage s t`, the inverse of `e` maps `t` to the preimage of `s` in `α`, i.e., `e⁻¹'(t) ∩ s = e(s) ∩ t`.
|
PartialEquiv.trans_refl
theorem PartialEquiv.trans_refl :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.trans (PartialEquiv.refl β) = e
The theorem `PartialEquiv.trans_refl` asserts that for all types `α` and `β`, and for any partial equivalence `e` from `α` to `β`, the composition of `e` with the identity partial equivalence on `β` (denoted as `PartialEquiv.refl β`) is equal to `e` itself. In other words, this theorem states that the identity partial equivalence acts as a right identity with respect to the composition of partial equivalences.
More concisely: For any partial equivalences `e: α ≃_* β` and `r: β ≃_* β` in Lean 4, `e �circ r = e`, where `�circ` denotes composition.
|
PartialEquiv.leftInvOn
theorem PartialEquiv.leftInvOn :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.LeftInvOn (↑e.symm) (↑e) e.source
The theorem `PartialEquiv.leftInvOn` states that for any partial equivalence `e` between two types `α` and `β`, the function `↑(PartialEquiv.symm e)` is a left inverse to the function `↑e` on the domain `e.source`. In other words, for all `x` in the domain `e.source`, applying `e` to `x` and then applying the inverse of `e` to the result will give you `x` back. This is a representation of the property that every element in the domain of a partial equivalence has a unique corresponding element in the target, and vice versa.
More concisely: For any partial equivalence relation `e` between types `α` and `β`, `↑(PartialEquiv.symm e) ∘ ↑e = id_α` on the domain `e.source`. Here, `id_α` denotes the identity function on type `α`.
|
Mathlib.Logic.Equiv.PartialEquiv._auxLemma.8
theorem Mathlib.Logic.Equiv.PartialEquiv._auxLemma.8 : ∀ {a b c : Prop}, (a ∧ b ↔ a ∧ c) = (a → (b ↔ c))
This theorem states that for any three propositions `a`, `b`, and `c`, the equivalence of `a ∧ b` and `a ∧ c` is the same as saying that if `a` is true, then `b` is equivalent to `c`. In other words, if the conjunction of `a` and `b` is equivalent to the conjunction of `a` and `c`, then `b` is equivalent to `c` assuming `a` is true.
More concisely: The theorem asserts that `(a ∧ b) ↔ (a ∧ c)` is equivalent to `(a → (b ↔ c))`.
|
PartialEquiv.trans_source''
theorem PartialEquiv.trans_source'' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
(e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
The theorem `PartialEquiv.trans_source''` asserts that for all partial equivalences `e` from type `α` to type `β`, and `e'` from type `β` to type `γ`, the source domain of the composition of `e` and `e'` (denoted as `PartialEquiv.trans e e'`) equals the image of the intersection of `e.target` and `e'.source` under the inverse of `e` (denoted as `PartialEquiv.symm e`). This is a property about the domain of definition when composing two partial equivalences.
More concisely: For all partial equivalences $e:\alpha \rightleftharpoons \beta$ and $e':\beta \rightleftharpoons \gamma$ in Lean 4, the domain of definition of $e \circ e'$ is equal to the image of $e'.source \cap e.target$ under the inverse of $e$.
|
PartialEquiv.rightInvOn
theorem PartialEquiv.rightInvOn :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.RightInvOn (↑e.symm) (↑e) e.target
The theorem `PartialEquiv.rightInvOn` states that for any partial equivalence `e` from type `α` to type `β`, the inverse function of `e` (obtained via `PartialEquiv.symm e`) is a right inverse to `e` on the target set of `e`. In other words, for all elements in the target set of `e`, if we apply `e` to the result of applying the inverse function of `e`, we get back the original element.
More concisely: For any partial equivalence relation `e` from type `α` to type `β`, the right inverse of `e` (obtained from `e.symm`) equals `e` on the target set of `e`.
|
PartialEquiv.right_inv
theorem PartialEquiv.right_inv :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β}, x ∈ e.target → ↑e (↑e.symm x) = x
This theorem states that for any partial equivalence `e` between two types `α` and `β`, and any element `x` of type `β` that lies in the target of `e`, applying the partial equivalence `e` to the result of applying the inverse of `e` (denoted as `PartialEquiv.symm e`) to `x`, results in `x` itself. In other words, it asserts the right inverse property for a partial equivalence, i.e., if we apply the function and then its inverse, we get back to the original element.
More concisely: For any partial equivalence `e` between types `α` and `β`, if `x` is in the target of `e`, then `e (x) = x ↔ ∃ y : α, e.symm x = y ∧ e y = x`.
|
PartialEquiv.image_source_eq_target
theorem PartialEquiv.image_source_eq_target :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), ↑e '' e.source = e.target
This theorem states that for every partial equivalence `e` between two types `α` and `β`, the image of the source set of `e` under the partial equivalence `e` is equal to the target set of `e`. In other words, if you take every element in the source of the partial equivalence and map it using `e`, you will get exactly the target set. This is a property that holds for every partial equivalence between two types.
More concisely: For every partial equivalence relation `e` between types `α` and `β`, the images of `α` under `e` and `e.eq` are equal, where `e.eq` is the equivalence classes formed by `e`. (Or, more succinctly: The source and target sets of a partial equivalence relation are equal.)
|
Mathlib.Logic.Equiv.PartialEquiv._auxLemma.3
theorem Mathlib.Logic.Equiv.PartialEquiv._auxLemma.3 :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β}, x ∈ e.target → (↑e.symm x ∈ e.source) = True := by
sorry
The theorem `Mathlib.Logic.Equiv.PartialEquiv._auxLemma.3` states that for any types `α` and `β`, and for any partial equivalence `e` between `α` and `β`, if an element `x` of type `β` is in the target of `e`, then the inverse of `e` (denoted `PartialEquiv.symm e`) applied to `x` is in the source of `e`. In other words, if `x` is in the range of the partial equivalence, then its preimage under the inverse equivalence is in the domain of the original partial equivalence.
More concisely: For any partial equivalence `e` between types `α` and `β`, if `x ∈ β` is in the image of `e`, then `PartialEquiv.symm e x ∈ α` is in the domain of `e`.
|
PartialEquiv.EqOnSource.eqOn
theorem PartialEquiv.EqOnSource.eqOn :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → Set.EqOn (↑e) (↑e') e.source
This theorem states that if two partial equivalences `e` and `e'` between types `α` and `β` are equivalent to each other, then the functions corresponding to `e` and `e'` are equal on the source set of `e`. In other words, for all elements `x` in the source of `e`, the results of applying `e` and `e'` to `x` are the same.
More concisely: If two partial equivalences `e` and `e'` from type `α` to type `β` are equal, then for all `x ∈ domain e`, `e x = e' x`.
|
PartialEquiv.prod_trans
theorem PartialEquiv.prod_trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {η : Type u_5} {ε : Type u_6} (e : PartialEquiv α β)
(f : PartialEquiv β γ) (e' : PartialEquiv δ η) (f' : PartialEquiv η ε),
(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
The theorem `PartialEquiv.prod_trans` states that for all types α, β, γ, δ, η, ε and given partial equivalences `e` from α to β, `f` from β to γ, `e'` from δ to η, and `f'` from η to ε, the composition of the product of `e` and `e'` with the product of `f` and `f'` is equal to the product of the composition of `e` and `f` with the composition of `e'` and `f'`. That is, it shows a certain commutativity property of the operations of composition and forming the product for partial equivalences.
More concisely: For all partial equivalences `e` from α to β, `f` from β to γ, `e'` from δ to η, and `f'` from η to ε, the composition of `e × e'` with `f × f'` is equal to the composition of `(e × f)` with `(e' × f')`.
|
PartialEquiv.EqOnSource.source_eq
theorem PartialEquiv.EqOnSource.source_eq :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → e.source = e'.source
This theorem states that if two partial equivalences, e and e', of types α and β are equivalent, then their sources are the same. In simple terms, for any two partial equivalences between two types, if they are equivalent, their starting points are identical. The sources of the partial equivalences, in this case, represent the subset of the first type from which the function is defined.
More concisely: If two partial equivalences `e : α ≃ β` and `e' : α' ≃ β'` are equivalent in Lean 4, then `α = α'`.
|
PartialEquiv.image_source_inter_eq'
theorem PartialEquiv.image_source_inter_eq' :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α),
↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
This theorem states that for any given partial equivalence `e` between types `α` and `β`, and for any set `s` of elements of type `α`, the image of the intersection between the source of `e` and `s` under `e` is equal to the intersection of the target of `e` and the pre-image of `s` under the inverse of `e`. In simpler words, this is about how intersections behave under the mapping of a partial equivalence and its inverse.
More concisely: Let `e` be a partial equivalence between types `α` and `β`, then `e''(α∩s) = β∩e′"(s)`, where `s` is a set of elements from `α`, `e''` is the image function of `e`, and `e'` is the inverse of `e`.
|
PartialEquiv.EqOnSource.restr
theorem PartialEquiv.EqOnSource.restr :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → ∀ (s : Set α), e.restr s ≈ e'.restr s := by
sorry
The theorem `PartialEquiv.EqOnSource.restr` expresses that for any two types `α` and `β` and any two partial equivalences `e` and `e'` between these types, if `e` and `e'` are equivalent, then restricting `e` and `e'` to a subset `s` of `α` preserves this equivalence. In other words, if two partial equivalences are equivalent overall, they remain equivalent even when limited to a specific set in the domain.
More concisely: If two partial equivalences between types `α` and `β` are equal, then their restrictions to a subset `s` of `α` are also equal.
|
Equiv.transPartialEquiv_eq_trans
theorem Equiv.transPartialEquiv_eq_trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f' : PartialEquiv β γ),
e.transPartialEquiv f' = e.toPartialEquiv.trans f'
This theorem states that for any types `α`, `β`, and `γ`, and any given equivalence `e` from `α` to `β` and a partial equivalence `f'` from `β` to `γ`, the operation of precomposing the partial equivalence `f'` with the equivalence `e` (using the `Equiv.transPartialEquiv` function) is the same as first converting the equivalence `e` to a partial equivalence (using the `Equiv.toPartialEquiv` function) and then composing this with `f'` (using the `PartialEquiv.trans` function). In other words, it's about the compatibility of the operations of precomposition and conversion to a partial equivalence with the operation of composition of partial equivalences.
More concisely: For any equivalences `e : α ≈ β` and partial equivalences `f' : β →* γ`, `Equiv.transPartialEquiv e f' = Equiv.toPartialEquiv e <<< f'`.
|
Equiv.trans_toPartialEquiv
theorem Equiv.trans_toPartialEquiv :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (e' : β ≃ γ),
(e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv
The theorem `Equiv.trans_toPartialEquiv` states that for any three types `α`, `β`, and `γ`, and any two equivalences `e` from `α` to `β` and `e'` from `β` to `γ`, the partial equivalence corresponding to the composition of `e` and `e'` (obtained using `Equiv.toPartialEquiv` on `e.trans e'`) is the same as the composition of the partial equivalences corresponding to `e` and `e'` (obtained by calling `PartialEquiv.trans` on `Equiv.toPartialEquiv e` and `Equiv.toPartialEquiv e'`). In other words, converting a composition of equivalences to a partial equivalence preserves the property of composition.
More concisely: For any equivalences e : α ≡ β and e' : β ≡ γ, Equiv.toPartialEquiv (e.trans e') = PartialEquiv.trans (Equiv.toPartialEquiv e) (Equiv.toPartialEquiv e').
|
PartialEquiv.IsImage.of_symm_preimage_eq
theorem PartialEquiv.IsImage.of_symm_preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t
This theorem states that for any arbitrary types `α` and `β`, given a partial equivalence `e` between `α` and `β`, and sets `s` of type `α` and `t` of type `β`, if the intersection of the target of `e` and the preimage of `s` under the inverse of `e` equals the intersection of the target of `e` and `t`, then `e` is said to be an image of `s` onto `t`. This is effectively an alias or another way to express the reverse direction of the theorem `PartialEquiv.IsImage.iff_symm_preimage_eq`.
More concisely: Given a partial equivalence `e` between types `α` and `β`, if the preimages of `s` under `e` and `e⁻¹` intersect `t` and its inverse image under `e` identically, then `e` maps `s` onto `t`.
|
PartialEquiv.self_trans_symm
theorem PartialEquiv.self_trans_symm :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.trans e.symm ≈ PartialEquiv.ofSet e.source
This theorem states that for any given partial equivalence `e` between types `α` and `β`, composing `e` with its inverse (i.e., `e.trans e.symm`) is equivalent to restricting the identity function to the source set of `e`. Here, the equivalence is defined in the sense of partial equivalences. Essentially, this result reflects the notion that applying a function and then its inverse brings us back to the original set, similar to the principle of identity in Mathematics.
More concisely: For any partial equivalence `e` between types `α` and `β`, `e.trans e.symm` is equal to the restriction of the identity function to the source set of `e`.
|
PartialEquiv.image_eq_target_inter_inv_preimage
theorem PartialEquiv.image_eq_target_inter_inv_preimage :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α},
s ⊆ e.source → ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
The theorem `PartialEquiv.image_eq_target_inter_inv_preimage` asserts that for any partial equivalence relation `e` of types `α` and `β`, and for any set `s` of type `α` that is a subset of the source of `e`, the image of `s` under `e` is equal to the intersection of the target of `e` and the preimage of `s` under the inverse of `e`. This theorem formalizes a basic property relating images and preimages under partial equivalences, which can be particularly useful in the study of relations and functions between different mathematical structures.
More concisely: For any partial equivalence relation `e` on types `α` and `β`, and any subset `s` of `α` in the source of `e`, the image of `s` under `e` is equal to the intersection of the target of `e` and the preimage of `s` under the inverse of `e`.
|
PartialEquiv.map_target'
theorem PartialEquiv.map_target' :
∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : β⦄, x ∈ self.target → self.invFun x ∈ self.source
This theorem, titled `PartialEquiv.map_target'`, states that for any given partial equivalence relation between two types `α` and `β`, if a particular element `x` from type `β` belongs to the target set of this partial equivalence relation, then the inverse function applied on `x` results in an element that belongs to the source set of the partial equivalence relation.
More concisely: For a partial equivalence relation between types `α` and `β`, if `x ∈ β` is related to some `y ∈ α` (i.e., `x ≈ y`), then the inverse function maps `x` to an element `z ∈ α` such that `z ≈ y`.
|
PartialEquiv.IsImage.mapsTo
theorem PartialEquiv.IsImage.mapsTo :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.IsImage s t → Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ t)
The theorem `PartialEquiv.IsImage.mapsTo` states that for any types `α` and `β`, any partial equivalence `e` between `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, if `t` is an image of `s` under the partial equivalence `e`, then the function represented by `e` maps each element of the intersection of the source of `e` and the set `s` to the intersection of the target of `e` and the set `t`. In other words, if an element is in both the source of `e` and `s`, its image under `e` will be in both the target of `e` and `t`.
More concisely: If a partial equivalence `e` maps set `s` to set `t`, then for all `x` in the intersection of the domain of `e` and `s`, `e(x)` is in the intersection of the range of `e` and `t`.
|
PartialEquiv.IsImage.symm
theorem PartialEquiv.IsImage.symm :
∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
e.IsImage s t → e.symm.IsImage t s
This theorem states that given any types `α` and `β`, a partial equivalence `e` between these types, and sets `s` of type `α` and `t` of type `β`, if `t` is an image of `s` under the partial equivalence `e`, then `s` is also an image of `t` under the inverse of the partial equivalence `e`. In other words, the image relationship under a partial equivalence and its inverse is symmetric.
More concisely: If `e` is a partial equivalence between types `α` and `β`, and `s` of type `α` is the image of `t` of type `β` under `e`, then `t` is the image of `s` under the inverse of `e`.
|
PartialEquiv.EqOnSource.target_eq
theorem PartialEquiv.EqOnSource.target_eq :
∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → e.target = e'.target
This theorem states that if two partial equivalences of types `α` and `β` are equivalent, then their targets are the same. In other words, for any two partial equivalences `e` and `e'` from `α` to `β`, if `e` is equivalent to `e'`, then the target of `e` equals to the target of `e'`.
More concisely: If two partial equivalences from type `α` to type `β` are equivalent in Lean 4, then they have the same target type `β`.
|
PartialEquiv.mapsTo
theorem PartialEquiv.mapsTo :
∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.MapsTo (↑e) e.source e.target
This theorem states that for any partial equivalence relation `e` between types `α` and `β`, the function from `α` to `β` determined by `e` maps every element of `e.source` to an element in `e.target`. In other words, all elements in the source of `e` are mapped to elements in the target of `e`, respecting the partial equivalence relation. Here, `Set.MapsTo` is a function that checks this property of mapping between sets.
More concisely: For any partial equivalence relation `e` between types `α` and `β`, the function determined by `e` maps every element in `e.source` to some element in `e.target`.
|
Mathlib.Logic.Equiv.PartialEquiv._auxLemma.6
theorem Mathlib.Logic.Equiv.PartialEquiv._auxLemma.6 :
∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b)
This theorem, named Mathlib.Logic.Equiv.PartialEquiv._auxLemma.6, states that for any type `α`, any element `x` of type `α`, and any two sets `a` and `b` of type `α`, the membership of `x` in the intersection of `a` and `b` is equivalent to `x` being a member of `a` and `x` being a member of `b`. This is conceptually similar to the mathematical set theory axiom that an element belongs to the intersection of two sets if and only if it belongs to both sets.
More concisely: For any type `α` and sets `a` and `b` of type `α`, the element `x` belongs to the intersection `a ∩ b` if and only if `x` belongs to both `a` and `b` (i.e., `x ∈ a ∧ x ∈ b`).
|
PartialEquiv.left_inv'
theorem PartialEquiv.left_inv' :
∀ {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : α⦄, x ∈ self.source → self.invFun (↑self x) = x := by
sorry
This theorem states that for any types `α` and `β`, and for any partial equivalence `self` between these types, if `x` is an element of the source of `self`, then applying the inverse function `invFun` to the result of applying `self` to `x` will yield `x` again. In other words, `invFun` undoes the application of `self` on elements in its source, acting as a left-inverse.
More concisely: For any partial equivalence `self` on types `α` and `β`, if `x ∈ α` and `self x ∈ domain self`, then `self.invFun (self x) = x`.
|
PartialEquiv.symm_symm
theorem PartialEquiv.symm_symm : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.symm = e
The theorem `PartialEquiv.symm_symm` states that for any partial equivalence `e` between two types `α` and `β`, applying the operation `PartialEquiv.symm` twice - that is, taking the "symmetry of the symmetry" - returns the original equivalence `e`. In other words, the double application of the symmetry operation on a partial equivalence is an identity operation.
More concisely: For any partial equivalence relation $e$ between types $\alpha$ and $\beta$, we have $e \circ \text{symm}(e) = \text{id}_{\alpha}$ and $\text{symm}(e) \circ e = \text{id}_{\beta}$, where $\text{symm}$ is the symmetry operation on partial equivalences and $\text{id}$ denotes the identity relation.
|