Mathlib.Logic.Equiv.PartialEquiv

mfld_cfg definition

: Simps.Config

Full source

/-- Common `@[simps]` configuration options used for manifold-related declarations. -/
def mfld_cfg : Simps.Config where
  attrs := [`mfld_simps]
  fullyApplied := false

Manifold simplification configuration

Informal description

The configuration `mfld_cfg` is a `Simps.Config` object used for specifying how `@[simps]` should generate simplification lemmas for manifold-related declarations. It is configured to use the `mfld_simps` attribute and does not require full application of the declarations.

Tactic.MfldSetTac.mfldSetTac definition

: Lean.ParserDescr✝

Full source

/-- A very basic tactic to show that sets showing up in manifolds coincide or are included
in one another. -/
elab (name := mfldSetTac) "mfld_set_tac" : tactic => withMainContext do
  let g ← getMainGoal
  let goalTy := (← instantiateMVars (← g.getDecl).type).getAppFnArgs
  match goalTy with
  | (``Eq, #[_ty, _e₁, _e₂]) =>
    evalTactic (← `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try simp only [*, mfld_simps] at h_my_y
          try simp only [*, mfld_simps])))
  | (``Subset, #[_ty, _inst, _e₁, _e₂]) =>
    evalTactic (← `(tactic| (
      intro my_y h_my_y
      try simp only [*, mfld_simps] at h_my_y
      try simp only [*, mfld_simps])))
  | _ => throwError "goal should be an equality or an inclusion"

Manifold set tactic

Informal description

A basic tactic called `mfld_set_tac` designed to prove equalities or inclusions of sets that appear in the context of manifolds. The tactic works by applying set extensionality for equality goals or introducing elements for subset goals, then simplifying using a specific set of simplification lemmas marked with the `mfld_simps` attribute.

PartialEquiv structure

(α : Type*) (β : Type*)

Full source

/-- Local equivalence between subsets `source` and `target` of `α` and `β` respectively. The
(global) maps `toFun : α → β` and `invFun : β → α` map `source` to `target` and conversely, and are
inverse to each other there. The values of `toFun` outside of `source` and of `invFun` outside of
`target` are irrelevant. -/
structure PartialEquiv (α : Type*) (β : Type*) where
  /-- The global function which has a partial inverse. Its value outside of the `source` subset is
  irrelevant. -/
  toFun : α → β
  /-- The partial inverse to `toFun`. Its value outside of the `target` subset is irrelevant. -/
  invFun : β → α
  /-- The domain of the partial equivalence. -/
  source : Set α
  /-- The codomain of the partial equivalence. -/
  target : Set β
  /-- The proposition that elements of `source` are mapped to elements of `target`. -/
  map_source' : ∀ ⦃x⦄, x ∈ source → toFun x ∈ target
  /-- The proposition that elements of `target` are mapped to elements of `source`. -/
  map_target' : ∀ ⦃x⦄, x ∈ target → invFun x ∈ source
  /-- The proposition that `invFun` is a left-inverse of `toFun` on `source`. -/
  left_inv' : ∀ ⦃x⦄, x ∈ source → invFun (toFun x) = x
  /-- The proposition that `invFun` is a right-inverse of `toFun` on `target`. -/
  right_inv' : ∀ ⦃x⦄, x ∈ target → toFun (invFun x) = x

Partial Equivalence Between Subsets

Informal description

A partial equivalence between types $\alpha$ and $\beta$ consists of two subsets $\text{source} \subseteq \alpha$ and $\text{target} \subseteq \beta$, along with two functions $\text{toFun} : \alpha \to \beta$ and $\text{invFun} : \beta \to \alpha$ that are inverses of each other when restricted to $\text{source}$ and $\text{target}$ respectively. The behavior of these functions outside their respective domains is irrelevant.

PartialEquiv.instInhabited instance

[Inhabited α] [Inhabited β] : Inhabited (PartialEquiv α β)

Full source

instance [Inhabited α] [Inhabited β] : Inhabited (PartialEquiv α β) :=
  ⟨⟨const α default, const β default, ∅, ∅, mapsTo_empty _ _, mapsTo_empty _ _, eqOn_empty _ _,
      eqOn_empty _ _⟩⟩

Inhabitedness of Partial Equivalences Between Inhabited Types

Informal description

For any inhabited types $\alpha$ and $\beta$, the type of partial equivalences between $\alpha$ and $\beta$ is also inhabited.

PartialEquiv.symm definition

: PartialEquiv β α

Full source

/-- The inverse of a partial equivalence -/
@[symm]
protected def symm : PartialEquiv β α where
  toFun := e.invFun
  invFun := e.toFun
  source := e.target
  target := e.source
  map_source' := e.map_target'
  map_target' := e.map_source'
  left_inv' := e.right_inv'
  right_inv' := e.left_inv'

Inverse of a partial equivalence

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse partial equivalence $e^{-1}$ is defined by swapping the source and target sets and interchanging the functions $\text{toFun}$ and $\text{invFun}$. Specifically: - The source of $e^{-1}$ is the target of $e$, - The target of $e^{-1}$ is the source of $e$, - The forward function of $e^{-1}$ is the inverse function of $e$, - The inverse function of $e^{-1}$ is the forward function of $e$. This construction ensures that $e^{-1}$ is indeed a partial equivalence from $\beta$ to $\alpha$, with the same inverse relationship as $e$.

PartialEquiv.instCoeFunForall instance

: CoeFun (PartialEquiv α β) fun _ => α → β

Full source

instance : CoeFun (PartialEquiv α β) fun _ => α → β :=
  ⟨PartialEquiv.toFun⟩

Coercion of Partial Equivalences to Functions

Informal description

For any types $\alpha$ and $\beta$, a partial equivalence $e$ between $\alpha$ and $\beta$ can be treated as a function from $\alpha$ to $\beta$ via the coercion $e(x) = e.\text{toFun}(x)$. This allows partial equivalences to be used directly as functions in expressions.

PartialEquiv.Simps.symm_apply definition

(e : PartialEquiv α β) : β → α

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (e : PartialEquiv α β) : β → α :=
  e.symm

Inverse function application for partial equivalence

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, the function `symm_apply` maps an element $y \in \beta$ to its preimage under $e$ (i.e., applies the inverse function of $e$ to $y$). This is equivalent to applying the inverse partial equivalence $e^{-1}$ to $y$.

PartialEquiv.coe_mk theorem

(f : α → β) (g s t ml mr il ir) : (PartialEquiv.mk f g s t ml mr il ir : α → β) = f

Full source

theorem coe_mk (f : α → β) (g s t ml mr il ir) :
    (PartialEquiv.mk f g s t ml mr il ir : α → β) = f := rfl

Coercion of Constructed Partial Equivalence Equals Original Function

Informal description

For any function $f : \alpha \to \beta$, function $g : \beta \to \alpha$, sets $s \subseteq \alpha$ and $t \subseteq \beta$, and proofs `ml`, `mr`, `il`, `ir` of the required properties, the coercion of the partial equivalence `PartialEquiv.mk f g s t ml mr il ir` to a function equals $f$. In other words, when treating the constructed partial equivalence as a function, it behaves exactly as $f$.

PartialEquiv.coe_symm_mk theorem

(f : α → β) (g s t ml mr il ir) : ((PartialEquiv.mk f g s t ml mr il ir).symm : β → α) = g

Full source

@[simp, mfld_simps]
theorem coe_symm_mk (f : α → β) (g s t ml mr il ir) :
    ((PartialEquiv.mk f g s t ml mr il ir).symm : β → α) = g :=
  rfl

Inverse of Constructed Partial Equivalence Coerces to Original Inverse Function

Informal description

For any functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$, subsets $s \subseteq \alpha$ and $t \subseteq \beta$, and proofs `ml`, `mr`, `il`, `ir` of the required properties, the coercion of the inverse of the partial equivalence `PartialEquiv.mk f g s t ml mr il ir` to a function equals $g$. In other words, when treating the inverse of the constructed partial equivalence as a function, it behaves exactly as $g$.

PartialEquiv.invFun_as_coe theorem

: e.invFun = e.symm

Full source

@[simp, mfld_simps]
theorem invFun_as_coe : e.invFun = e.symm :=
  rfl

Inverse Function as Coercion of Symmetric Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse function $e.\text{invFun}$ is equal to the coercion of the inverse partial equivalence $e^{-1}$ (i.e., $e.\text{symm}$) to a function. In other words, $e.\text{invFun} = e^{-1}$ as functions from $\beta$ to $\alpha$.

PartialEquiv.map_source theorem

{x : α} (h : x ∈ e.source) : e x ∈ e.target

Full source

@[simp, mfld_simps]
theorem map_source {x : α} (h : x ∈ e.source) : e x ∈ e.target :=
  e.map_source' h

Image of Source Element Belongs to Target in Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, if $x \in \alpha$ belongs to the source set $e.\text{source}$, then the image of $x$ under $e$ belongs to the target set $e.\text{target}$, i.e., $e(x) \in e.\text{target}$.

PartialEquiv.map_source'' theorem

: e '' e.source ⊆ e.target

Full source

/-- Variant of `e.map_source` and `map_source'`, stated for images of subsets of `source`. -/
lemma map_source'' : e '' e.sourcee '' e.source ⊆ e.target :=
  fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)

Image of Source is Subset of Target in Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the image of the source set $e.\text{source}$ under the function $e$ is contained in the target set $e.\text{target}$, i.e., $e(e.\text{source}) \subseteq e.\text{target}$.

PartialEquiv.map_target theorem

{x : β} (h : x ∈ e.target) : e.symm x ∈ e.source

Full source

@[simp, mfld_simps]
theorem map_target {x : β} (h : x ∈ e.target) : e.symm x ∈ e.source :=
  e.map_target' h

Inverse Image of Target Element Belongs to Source in Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, if $x \in \beta$ belongs to the target set $e.\text{target}$, then the image of $x$ under the inverse partial equivalence $e^{-1}$ belongs to the source set $e.\text{source}$, i.e., $e^{-1}(x) \in e.\text{source}$.

PartialEquiv.left_inv theorem

{x : α} (h : x ∈ e.source) : e.symm (e x) = x

Full source

@[simp, mfld_simps]
theorem left_inv {x : α} (h : x ∈ e.source) : e.symm (e x) = x :=
  e.left_inv' h

Left Inverse Property of Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, and for any element $x \in \alpha$ in the source set $e.\text{source}$, the composition of $e$ followed by its inverse $e^{-1}$ maps $x$ back to itself, i.e., $e^{-1}(e(x)) = x$.

PartialEquiv.right_inv theorem

{x : β} (h : x ∈ e.target) : e (e.symm x) = x

Full source

@[simp, mfld_simps]
theorem right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x :=
  e.right_inv' h

Right Inverse Property of Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, and for any element $x \in \beta$ in the target set $e.\text{target}$, the composition of the inverse $e^{-1}$ followed by $e$ maps $x$ back to itself, i.e., $e(e^{-1}(x)) = x$.

PartialEquiv.mapsTo theorem

: MapsTo e e.source e.target

Full source

protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source

Mapping Property of Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the function $e$ maps every element of its source set $e.\text{source} \subseteq \alpha$ to an element of its target set $e.\text{target} \subseteq \beta$.

PartialEquiv.symm_mapsTo theorem

: MapsTo e.symm e.target e.source

Full source

theorem symm_mapsTo : MapsTo e.symm e.target e.source :=
  e.symm.mapsTo

Inverse Partial Equivalence Preserves Target-to-Source Mapping

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse function $e^{-1}$ maps every element of the target set $e.\text{target} \subseteq \beta$ back to an element of the source set $e.\text{source} \subseteq \alpha$.

PartialEquiv.leftInvOn theorem

: LeftInvOn e.symm e e.source

Full source

protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun _ => e.left_inv

Left Inverse Property of Partial Equivalence on Source

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse function $e^{-1}$ is a left inverse of $e$ on the source set $e.\text{source} \subseteq \alpha$. That is, for all $x \in e.\text{source}$, we have $e^{-1}(e(x)) = x$.

PartialEquiv.rightInvOn theorem

: RightInvOn e.symm e e.target

Full source

protected theorem rightInvOn : RightInvOn e.symm e e.target := fun _ => e.right_inv

Right Inverse Property of Partial Equivalence on Target Set

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse function $e^{-1}$ is a right inverse of $e$ on the target set $e.\text{target} \subseteq \beta$. That is, for all $x \in e.\text{target}$, we have $e(e^{-1}(x)) = x$.

PartialEquiv.invOn theorem

: InvOn e.symm e e.source e.target

Full source

protected theorem invOn : InvOn e.symm e e.source e.target :=
  ⟨e.leftInvOn, e.rightInvOn⟩

Inverse Property of Partial Equivalence on Source and Target

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse function $e^{-1}$ is both a left inverse on the source set $e.\text{source} \subseteq \alpha$ and a right inverse on the target set $e.\text{target} \subseteq \beta$. That is: 1. For all $x \in e.\text{source}$, we have $e^{-1}(e(x)) = x$. 2. For all $y \in e.\text{target}$, we have $e(e^{-1}(y)) = y$.

PartialEquiv.injOn theorem

: InjOn e e.source

Full source

protected theorem injOn : InjOn e e.source :=
  e.leftInvOn.injOn

Injectivity of Partial Equivalence on Source Set

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the function $e$ is injective on its source set $e.\text{source} \subseteq \alpha$. That is, for any $x, y \in e.\text{source}$, if $e(x) = e(y)$, then $x = y$.

PartialEquiv.bijOn theorem

: BijOn e e.source e.target

Full source

protected theorem bijOn : BijOn e e.source e.target :=
  e.invOn.bijOn e.mapsTo e.symm_mapsTo

Bijectivity of Partial Equivalence on Source and Target

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the function $e$ is bijective when restricted to its source set $e.\text{source} \subseteq \alpha$ and target set $e.\text{target} \subseteq \beta$. That is: 1. $e$ is injective on $e.\text{source}$, 2. $e$ is surjective from $e.\text{source}$ to $e.\text{target}$.

PartialEquiv.surjOn theorem

: SurjOn e e.source e.target

Full source

protected theorem surjOn : SurjOn e e.source e.target :=
  e.bijOn.surjOn

Surjectivity of Partial Equivalence on Target Set

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the function $e$ is surjective from its source set $e.\text{source} \subseteq \alpha$ to its target set $e.\text{target} \subseteq \beta$. That is, for every $y \in e.\text{target}$, there exists an $x \in e.\text{source}$ such that $e(x) = y$.

Equiv.toPartialEquivOfImageEq definition

(e : α ≃ β) (s : Set α) (t : Set β) (h : e '' s = t) : PartialEquiv α β

Full source

/-- Interpret an `Equiv` as a `PartialEquiv` by restricting it to `s` in the domain
and to `t` in the codomain. -/
@[simps -fullyApplied]
def _root_.Equiv.toPartialEquivOfImageEq (e : α ≃ β) (s : Set α) (t : Set β) (h : e '' s = t) :
    PartialEquiv α β where
  toFun := e
  invFun := e.symm
  source := s
  target := t
  map_source' _ hx := h ▸ mem_image_of_mem _ hx
  map_target' x hx := by
    subst t
    rcases hx with ⟨x, hx, rfl⟩
    rwa [e.symm_apply_apply]
  left_inv' x _ := e.symm_apply_apply x
  right_inv' x _ := e.apply_symm_apply x

Restriction of an equivalence to subsets with matching image

Informal description

Given an equivalence (bijection) $e : \alpha \simeq \beta$, a subset $s \subseteq \alpha$, and a subset $t \subseteq \beta$ such that the image of $s$ under $e$ equals $t$ (i.e., $e(s) = t$), this constructs a partial equivalence between $\alpha$ and $\beta$ where: - The forward function is $e$ restricted to $s$, - The inverse function is $e^{-1}$ restricted to $t$, - The source is $s$, - The target is $t$. The functions $e$ and $e^{-1}$ are mutual inverses when restricted to $s$ and $t$ respectively.

Equiv.toPartialEquiv definition

(e : α ≃ β) : PartialEquiv α β

Full source

/-- Associate a `PartialEquiv` to an `Equiv`. -/
@[simps! (config := mfld_cfg)]
def _root_.Equiv.toPartialEquiv (e : α ≃ β) : PartialEquiv α β :=
  e.toPartialEquivOfImageEq univ univ <| by rw [image_univ, e.surjective.range_eq]

Total equivalence as a partial equivalence

Informal description

Given a bijective map $e : \alpha \simeq \beta$, this constructs a partial equivalence between $\alpha$ and $\beta$ where: - The forward function is $e$ restricted to the entire set $\alpha$ (source), - The inverse function is $e^{-1}$ restricted to the entire set $\beta$ (target), - The source is $\alpha$, - The target is $\beta$. The functions $e$ and $e^{-1}$ are mutual inverses when restricted to $\alpha$ and $\beta$ respectively.

PartialEquiv.inhabitedOfEmpty instance

[IsEmpty α] [IsEmpty β] : Inhabited (PartialEquiv α β)

Full source

instance inhabitedOfEmpty [IsEmpty α] [IsEmpty β] : Inhabited (PartialEquiv α β) :=
  ⟨((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).toPartialEquiv⟩

Partial Equivalence Between Empty Types

Informal description

For any empty types $\alpha$ and $\beta$, there exists a canonical partial equivalence between them.

PartialEquiv.copy definition

 (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α) (hs : e.source = s)
  (t : Set β) (ht : e.target = t) : PartialEquiv α β

Full source

/-- Create a copy of a `PartialEquiv` providing better definitional equalities. -/
@[simps -fullyApplied]
def copy (e : PartialEquiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g) (s : Set α)
    (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    PartialEquiv α β where
  toFun := f
  invFun := g
  source := s
  target := t
  map_source' _ := ht ▸ hs ▸ hf ▸ e.map_source
  map_target' _ := hs ▸ ht ▸ hg ▸ e.map_target
  left_inv' _ := hs ▸ hf ▸ hg ▸ e.left_inv
  right_inv' _ := ht ▸ hf ▸ hg ▸ e.right_inv

Copy of a partial equivalence with specified components

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, a function $f : \alpha \to \beta$ equal to $e$'s forward map, a function $g : \beta \to \alpha$ equal to $e$'s inverse map, a set $s \subseteq \alpha$ equal to $e$'s source, and a set $t \subseteq \beta$ equal to $e$'s target, this constructs a new partial equivalence with these specified components. The new partial equivalence has: - Forward map $f$, - Inverse map $g$, - Source set $s$, - Target set $t$, while maintaining the same partial inverse properties as $e$.

PartialEquiv.copy_eq theorem

 (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

Full source

theorem copy_eq (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 := by
  substs f g s t
  cases e
  rfl

Equality of Partial Equivalence Copy with Original

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$ such that $f$ equals $e$'s forward map and $g$ equals $e$'s inverse map, and sets $s \subseteq \alpha$ and $t \subseteq \beta$ such that $s$ equals $e$'s source and $t$ equals $e$'s target, then the constructed copy of $e$ with these specified components is equal to $e$ itself.

PartialEquiv.toEquiv definition

: e.source ≃ e.target

Full source

/-- Associate to a `PartialEquiv` an `Equiv` between the source and the target. -/
protected def toEquiv : e.source ≃ e.target where
  toFun x := ⟨e x, e.map_source x.mem⟩
  invFun y := ⟨e.symm y, e.map_target y.mem⟩
  left_inv := fun ⟨_, hx⟩ => Subtype.eq <| e.left_inv hx
  right_inv := fun ⟨_, hy⟩ => Subtype.eq <| e.right_inv hy

Equivalence between source and target of a partial equivalence

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, the function constructs an equivalence (bijection) between the source set $e.\text{source} \subseteq \alpha$ and the target set $e.\text{target} \subseteq \beta$. Specifically: - The forward map sends $x \in e.\text{source}$ to $e(x) \in e.\text{target}$. - The inverse map sends $y \in e.\text{target}$ to $e^{-1}(y) \in e.\text{source}$. - These maps are mutual inverses, satisfying $e^{-1}(e(x)) = x$ for all $x \in e.\text{source}$ and $e(e^{-1}(y)) = y$ for all $y \in e.\text{target}$.

PartialEquiv.symm_source theorem

: e.symm.source = e.target

Full source

@[simp, mfld_simps]
theorem symm_source : e.symm.source = e.target :=
  rfl

Source of Inverse Equals Target of Original Partial Equivalence

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the source set of its inverse $e^{-1}$ equals the target set of $e$, i.e., $e^{-1}.\text{source} = e.\text{target}$.

PartialEquiv.symm_target theorem

: e.symm.target = e.source

Full source

@[simp, mfld_simps]
theorem symm_target : e.symm.target = e.source :=
  rfl

Inverse Partial Equivalence Target Equals Original Source

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the target set of its inverse $e^{-1}$ is equal to the source set of $e$, i.e., $e^{-1}.\text{target} = e.\text{source}$.

PartialEquiv.symm_symm theorem

: e.symm.symm = e

Full source

@[simp, mfld_simps]
theorem symm_symm : e.symm.symm = e := rfl

Double Inverse of Partial Equivalence is Identity

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the inverse of the inverse of $e$ is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

PartialEquiv.symm_bijective theorem

: Function.Bijective (PartialEquiv.symm : PartialEquiv α β → PartialEquiv β α)

Full source

theorem symm_bijective :
    Function.Bijective (PartialEquiv.symm : PartialEquiv α β → PartialEquiv β α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Partial Equivalences

Informal description

The inverse operation `symm` on partial equivalences, which maps a partial equivalence $e : \alpha \to \beta$ to its inverse $e^{-1} : \beta \to \alpha$, is a bijective function from the set of partial equivalences between $\alpha$ and $\beta$ to the set of partial equivalences between $\beta$ and $\alpha$.

PartialEquiv.image_source_eq_target theorem

: e '' e.source = e.target

Full source

theorem image_source_eq_target : e '' e.source = e.target :=
  e.bijOn.image_eq

Image of Source Equals Target in Partial Equivalence

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the image of the source set $e.\text{source} \subseteq \alpha$ under $e$ is equal to the target set $e.\text{target} \subseteq \beta$, i.e., $e(e.\text{source}) = e.\text{target}$.

PartialEquiv.forall_mem_target theorem

{p : β → Prop} : (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (e x)

Full source

theorem forall_mem_target {p : β → Prop} : (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (e x) := by
  rw [← image_source_eq_target, forall_mem_image]

Universal Quantification over Target vs. Source in Partial Equivalence

Informal description

For any predicate $p$ on $\beta$, the statement that $p(y)$ holds for all $y$ in the target set $e.\text{target}$ is equivalent to the statement that $p(e(x))$ holds for all $x$ in the source set $e.\text{source}$.

PartialEquiv.exists_mem_target theorem

{p : β → Prop} : (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (e x)

Full source

theorem exists_mem_target {p : β → Prop} : (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (e x) := by
  rw [← image_source_eq_target, exists_mem_image]

Existence in Target of Partial Equivalence Corresponds to Existence in Source

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any predicate $p$ on $\beta$, there exists an element $y$ in the target of $e$ satisfying $p(y)$ if and only if there exists an element $x$ in the source of $e$ such that $p(e(x))$ holds.

PartialEquiv.IsImage definition

(s : Set α) (t : Set β) : Prop

Full source

/-- We say that `t : Set β` is an image of `s : Set α` under a partial equivalence if
any of the following equivalent conditions hold:

* `e '' (e.source ∩ s) = e.target ∩ t`;
* `e.source ∩ e ⁻¹ t = e.source ∩ s`;
* `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
-/
def IsImage (s : Set α) (t : Set β) : Prop :=
  ∀ ⦃x⦄, x ∈ e.source → (e x ∈ te x ∈ t ↔ x ∈ s)

Image condition for partial equivalence

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, we say that a subset $t \subseteq \beta$ is the image of a subset $s \subseteq \alpha$ under $e$ if for every $x$ in the source of $e$, the image $e(x)$ belongs to $t$ if and only if $x$ belongs to $s$.

PartialEquiv.IsImage.apply_mem_iff theorem

(h : e.IsImage s t) (hx : x ∈ e.source) : e x ∈ t ↔ x ∈ s

Full source

theorem apply_mem_iff (h : e.IsImage s t) (hx : x ∈ e.source) : e x ∈ te x ∈ t ↔ x ∈ s :=
  h hx

Image Condition Characterization for Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$, $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under $e$. Then for any $x$ in the source of $e$, we have $e(x) \in t$ if and only if $x \in s$.

PartialEquiv.IsImage.symm_apply_mem_iff theorem

(h : e.IsImage s t) : ∀ ⦃y⦄, y ∈ e.target → (e.symm y ∈ s ↔ y ∈ t)

Full source

theorem symm_apply_mem_iff (h : e.IsImage s t) : ∀ ⦃y⦄, y ∈ e.target → (e.symm y ∈ se.symm y ∈ s ↔ y ∈ t) :=
  e.forall_mem_target.mpr fun x hx => by rw [e.left_inv hx, h hx]

Inverse Image Characterization for Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under $e$ (i.e., $e.\text{IsImage}~s~t$ holds). Then for any $y$ in the target of $e$, the inverse image $e^{-1}(y)$ belongs to $s$ if and only if $y$ belongs to $t$.

PartialEquiv.IsImage.symm theorem

(h : e.IsImage s t) : e.symm.IsImage t s

Full source

protected theorem symm (h : e.IsImage s t) : e.symm.IsImage t s :=
  h.symm_apply_mem_iff

Inverse Image Symmetry for Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under $e$. Then the inverse partial equivalence $e^{-1}$ has $s$ as the image of $t$.

PartialEquiv.IsImage.symm_iff theorem

: e.symm.IsImage t s ↔ e.IsImage s t

Full source

@[simp]
theorem symm_iff : e.symm.IsImage t s ↔ e.IsImage s t :=
  ⟨fun h => h.symm, fun h => h.symm⟩

Equivalence of Image Conditions for Partial Equivalence and Its Inverse

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, and subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the following are equivalent: 1. The inverse partial equivalence $e^{-1}$ maps $t$ to $s$ (i.e., $e^{-1}.\text{IsImage}~t~s$ holds). 2. The partial equivalence $e$ maps $s$ to $t$ (i.e., $e.\text{IsImage}~s~t$ holds).

PartialEquiv.IsImage.mapsTo theorem

(h : e.IsImage s t) : MapsTo e (e.source ∩ s) (e.target ∩ t)

Full source

protected theorem mapsTo (h : e.IsImage s t) : MapsTo e (e.source ∩ s) (e.target ∩ t) :=
  fun _ hx => ⟨e.mapsTo hx.1, (h hx.1).2 hx.2⟩

Mapping Property of Partial Equivalence on Restricted Domains

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and suppose that a subset $t \subseteq \beta$ is the image of a subset $s \subseteq \alpha$ under $e$. Then the function $e$ maps every element in the intersection of its source set $e.\text{source}$ with $s$ to an element in the intersection of its target set $e.\text{target}$ with $t$.

PartialEquiv.IsImage.symm_mapsTo theorem

(h : e.IsImage s t) : MapsTo e.symm (e.target ∩ t) (e.source ∩ s)

Full source

theorem symm_mapsTo (h : e.IsImage s t) : MapsTo e.symm (e.target ∩ t) (e.source ∩ s) :=
  h.symm.mapsTo

Inverse Mapping Property of Partial Equivalence on Restricted Domains

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and suppose that a subset $t \subseteq \beta$ is the image of a subset $s \subseteq \alpha$ under $e$. Then the inverse function $e^{-1}$ maps every element in the intersection of the target set $e.\text{target}$ with $t$ to an element in the intersection of the source set $e.\text{source}$ with $s$.

PartialEquiv.IsImage.restr definition

(h : e.IsImage s t) : PartialEquiv α β

Full source

/-- Restrict a `PartialEquiv` to a pair of corresponding sets. -/
@[simps -fullyApplied]
def restr (h : e.IsImage s t) : PartialEquiv α β where
  toFun := e
  invFun := e.symm
  source := e.source ∩ s
  target := e.target ∩ t
  map_source' := h.mapsTo
  map_target' := h.symm_mapsTo
  left_inv' := e.leftInvOn.mono inter_subset_left
  right_inv' := e.rightInvOn.mono inter_subset_left

Restriction of a partial equivalence to corresponding subsets

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, and subsets $s \subseteq \alpha$, $t \subseteq \beta$ such that $t$ is the image of $s$ under $e$, the restricted partial equivalence $e \restriction_{s,t}$ is defined with: - Source set: $e.\text{source} \cap s$ - Target set: $e.\text{target} \cap t$ - Forward function: $e \restriction_{e.\text{source} \cap s}$ - Inverse function: $e^{-1} \restriction_{e.\text{target} \cap t}$ The restricted partial equivalence maintains the inverse relationship between its forward and inverse functions on their respective restricted domains.

PartialEquiv.IsImage.image_eq theorem

(h : e.IsImage s t) : e '' (e.source ∩ s) = e.target ∩ t

Full source

theorem image_eq (h : e.IsImage s t) : e '' (e.source ∩ s) = e.target ∩ t :=
  h.restr.image_source_eq_target

Image of Restricted Source Equals Restricted Target in Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under $e$ (i.e., $e.\text{IsImage}\ s\ t$ holds). Then the image of the intersection $e.\text{source} \cap s$ under $e$ equals the intersection $e.\text{target} \cap t$, i.e., $e(e.\text{source} \cap s) = e.\text{target} \cap t$.

PartialEquiv.IsImage.symm_image_eq theorem

(h : e.IsImage s t) : e.symm '' (e.target ∩ t) = e.source ∩ s

Full source

theorem symm_image_eq (h : e.IsImage s t) : e.symm '' (e.target ∩ t) = e.source ∩ s :=
  h.symm.image_eq

Inverse Image of Restricted Target Equals Restricted Source in Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under $e$. Then the image of the intersection $e.\text{target} \cap t$ under the inverse partial equivalence $e^{-1}$ equals the intersection $e.\text{source} \cap s$, i.e., $e^{-1}(e.\text{target} \cap t) = e.\text{source} \cap s$.

PartialEquiv.IsImage.iff_preimage_eq theorem

: e.IsImage s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s

Full source

theorem iff_preimage_eq : e.IsImage s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s := by
  simp only [IsImage, Set.ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]

Characterization of Partial Equivalence Image via Preimage Equality

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the following are equivalent: 1. $t$ is the image of $s$ under $e$ (i.e., for $x \in e.\text{source}$, $e(x) \in t$ if and only if $x \in s$) 2. The preimage of $t$ under $e$ intersected with $e.\text{source}$ equals $s$ intersected with $e.\text{source}$ In other words, $e.\text{IsImage}\ s\ t$ holds if and only if $e.\text{source} \cap e^{-1}(t) = e.\text{source} \cap s$.

PartialEquiv.IsImage.iff_symm_preimage_eq theorem

: e.IsImage s t ↔ e.target ∩ e.symm ⁻¹' s = e.target ∩ t

Full source

theorem iff_symm_preimage_eq : e.IsImage s t ↔ e.target ∩ e.symm ⁻¹' s = e.target ∩ t :=
  symm_iff.symm.trans iff_preimage_eq

Characterization of Partial Equivalence Image via Inverse Preimage Equality

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the following are equivalent: 1. $t$ is the image of $s$ under $e$ (i.e., $e.\text{IsImage}\ s\ t$ holds) 2. The preimage of $s$ under $e^{-1}$ intersected with $e.\text{target}$ equals $t$ intersected with $e.\text{target}$ In other words, $e.\text{IsImage}\ s\ t$ holds if and only if $e.\text{target} \cap e^{-1}(s) = e.\text{target} \cap t$.

PartialEquiv.IsImage.of_image_eq theorem

(h : e '' (e.source ∩ s) = e.target ∩ t) : e.IsImage s t

Full source

theorem of_image_eq (h : e '' (e.source ∩ s) = e.target ∩ t) : e.IsImage s t :=
  of_symm_preimage_eq <| Eq.trans (of_symm_preimage_eq rfl).image_eq.symm h

Image Condition for Partial Equivalence via Restricted Image Equality

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets. If the image of $e.\text{source} \cap s$ under $e$ equals $e.\text{target} \cap t$, then $t$ is the image of $s$ under $e$ (i.e., $e.\text{IsImage}\ s\ t$ holds).

PartialEquiv.IsImage.of_symm_image_eq theorem

(h : e.symm '' (e.target ∩ t) = e.source ∩ s) : e.IsImage s t

Full source

theorem of_symm_image_eq (h : e.symm '' (e.target ∩ t) = e.source ∩ s) : e.IsImage s t :=
  of_preimage_eq <| Eq.trans (iff_preimage_eq.2 rfl).symm_image_eq.symm h

Image Condition via Inverse Image Equality in Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, with subsets $s \subseteq \alpha$ and $t \subseteq \beta$. If the image of $e.\text{target} \cap t$ under the inverse partial equivalence $e^{-1}$ equals $e.\text{source} \cap s$, then $t$ is the image of $s$ under $e$ (i.e., $e.\text{IsImage}\ s\ t$ holds).

PartialEquiv.IsImage.compl theorem

(h : e.IsImage s t) : e.IsImage sᶜ tᶜ

Full source

protected theorem compl (h : e.IsImage s t) : e.IsImage sᶜ tᶜ := fun _ hx => not_congr (h hx)

Image of Complement under Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets. If $t$ is the image of $s$ under $e$, then the complement $t^c$ is the image of the complement $s^c$ under $e$.

PartialEquiv.IsImage.inter theorem

{s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∩ s') (t ∩ t')

Full source

protected theorem inter {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') :
    e.IsImage (s ∩ s') (t ∩ t') := fun _ hx => and_congr (h hx) (h' hx)

Image of Intersection under Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s, s' \subseteq \alpha$ and $t, t' \subseteq \beta$ be subsets. If $t$ is the image of $s$ under $e$ and $t'$ is the image of $s'$ under $e$, then the intersection $t \cap t'$ is the image of the intersection $s \cap s'$ under $e$.

PartialEquiv.IsImage.union theorem

{s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∪ s') (t ∪ t')

Full source

protected theorem union {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') :
    e.IsImage (s ∪ s') (t ∪ t') := fun _ hx => or_congr (h hx) (h' hx)

Image of Union under Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s, s' \subseteq \alpha$ and $t, t' \subseteq \beta$ be subsets. If $t$ is the image of $s$ under $e$ and $t'$ is the image of $s'$ under $e$, then the union $t \cup t'$ is the image of the union $s \cup s'$ under $e$.

PartialEquiv.IsImage.diff theorem

{s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s \ s') (t \ t')

Full source

protected theorem diff {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') :
    e.IsImage (s \ s') (t \ t') :=
  h.inter h'.compl

Image of Set Difference under Partial Equivalence

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s, s' \subseteq \alpha$ and $t, t' \subseteq \beta$ be subsets. If $t$ is the image of $s$ under $e$ and $t'$ is the image of $s'$ under $e$, then the set difference $t \setminus t'$ is the image of the set difference $s \setminus s'$ under $e$.

PartialEquiv.IsImage.leftInvOn_piecewise theorem

 {e' : PartialEquiv α β} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) :
  LeftInvOn (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source)

Full source

theorem leftInvOn_piecewise {e' : PartialEquiv α β} [∀ i, Decidable (i ∈ s)]
    [∀ i, Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) :
    LeftInvOn (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source) := by
  rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩)
  · rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
  · rw [piecewise_eq_of_not_mem _ _ _ hs, piecewise_eq_of_not_mem _ _ _ ((h'.compl he).2 hs),
      e'.left_inv he]

Left Inverse Property for Piecewise-Defined Partial Equivalences on Image Sets

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under both $e$ and $e'$. Then the piecewise-defined function \[ f(x) = \begin{cases} e(x) & \text{if } x \in s, \\ e'(x) & \text{otherwise}, \end{cases} \] has a left inverse on the set $s.\text{ite}\ e.\text{source}\ e'.\text{source}$ (which equals $e.\text{source}$ when $x \in s$ and $e'.\text{source}$ otherwise) given by the piecewise function \[ g(y) = \begin{cases} e^{-1}(y) & \text{if } y \in t, \\ e'^{-1}(y) & \text{otherwise}. \end{cases} \]

PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn theorem

 {e' : PartialEquiv α β} (h : e.IsImage s t) (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s)
  (heq : EqOn e e' (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t

Full source

theorem inter_eq_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t)
    (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (heq : EqOn e e' (e.source ∩ s)) :
    e.target ∩ t = e'.target ∩ t := by rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]

Equality of Target Intersections for Partial Equivalences with Matching Source Behavior

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under both $e$ and $e'$. If the intersections $e.\text{source} \cap s$ and $e'.\text{source} \cap s$ are equal, and $e$ and $e'$ coincide on this intersection, then the intersections $e.\text{target} \cap t$ and $e'.\text{target} \cap t$ are also equal.

PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn theorem

 {e' : PartialEquiv α β} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (heq : EqOn e e' (e.source ∩ s)) :
  EqOn e.symm e'.symm (e.target ∩ t)

Full source

theorem symm_eq_on_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t)
    (hs : e.source ∩ s = e'.source ∩ s) (heq : EqOn e e' (e.source ∩ s)) :
    EqOn e.symm e'.symm (e.target ∩ t) := by
  rw [← h.image_eq]
  rintro y ⟨x, hx, rfl⟩
  have hx' := hx; rw [hs] at hx'
  rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]

Inverse Functions Coincide on Target Intersection When Partial Equivalences Agree on Source Intersection

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be subsets such that $t$ is the image of $s$ under $e$ (i.e., $e.\text{IsImage}\ s\ t$ holds). If the intersections $e.\text{source} \cap s$ and $e'.\text{source} \cap s$ are equal, and if $e$ and $e'$ coincide on this intersection, then their inverse functions $e^{-1}$ and $e'^{-1}$ coincide on the intersection $e.\text{target} \cap t$.

PartialEquiv.isImage_source_target theorem

: e.IsImage e.source e.target

Full source

theorem isImage_source_target : e.IsImage e.source e.target := fun x hx => by simp [hx]

Source and Target are Images Under Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the target set $e.target$ is the image of the source set $e.source$ under $e$. In other words, $e$ maps $e.source$ bijectively onto $e.target$.

PartialEquiv.isImage_source_target_of_disjoint theorem

 (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) :
  e.IsImage e'.source e'.target

Full source

theorem isImage_source_target_of_disjoint (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
    (ht : Disjoint e.target e'.target) : e.IsImage e'.source e'.target :=
  IsImage.of_image_eq <| by rw [hs.inter_eq, ht.inter_eq, image_empty]

Disjoint Partial Equivalences Preserve Image Property

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$. If the sources of $e$ and $e'$ are disjoint (i.e., $e.\text{source} \cap e'.\text{source} = \emptyset$) and their targets are also disjoint (i.e., $e.\text{target} \cap e'.\text{target} = \emptyset$), then the target of $e'$ is the image of the source of $e'$ under $e$ (i.e., $e.\text{IsImage}\ e'.\text{source}\ e'.\text{target}$ holds).

PartialEquiv.image_source_inter_eq' theorem

(s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s

Full source

theorem image_source_inter_eq' (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s := by
  rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]

Image of Source Intersection Equals Target Intersection with Inverse Preimage

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$, the image of the intersection $e.\text{source} \cap s$ under $e$ equals the intersection of $e.\text{target}$ with the preimage of $s$ under $e^{-1}$, i.e., $$ e(e.\text{source} \cap s) = e.\text{target} \cap e^{-1}(s). $$

PartialEquiv.image_source_inter_eq theorem

(s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' (e.source ∩ s)

Full source

theorem image_source_inter_eq (s : Set α) :
    e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' (e.source ∩ s) := by
  rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]

Image of Source Intersection Equals Target Intersection with Inverse Preimage

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$, the image of the intersection $e.\text{source} \cap s$ under $e$ equals the intersection of $e.\text{target}$ with the preimage of $e.\text{source} \cap s$ under the inverse function $e^{-1}$. In symbols: $$ e(e.\text{source} \cap s) = e.\text{target} \cap e^{-1}(e.\text{source} \cap s). $$

PartialEquiv.image_eq_target_inter_inv_preimage theorem

{s : Set α} (h : s ⊆ e.source) : e '' s = e.target ∩ e.symm ⁻¹' s

Full source

theorem image_eq_target_inter_inv_preimage {s : Set α} (h : s ⊆ e.source) :
    e '' s = e.target ∩ e.symm ⁻¹' s := by
  rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]

Image of Subset Equals Target Intersection with Inverse Preimage

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$ such that $s \subseteq e.\text{source}$, the image of $s$ under $e$ equals the intersection of $e.\text{target}$ with the preimage of $s$ under the inverse partial equivalence $e^{-1}$. In symbols: $$ e(s) = e.\text{target} \cap e^{-1}(s). $$

PartialEquiv.symm_image_eq_source_inter_preimage theorem

{s : Set β} (h : s ⊆ e.target) : e.symm '' s = e.source ∩ e ⁻¹' s

Full source

theorem symm_image_eq_source_inter_preimage {s : Set β} (h : s ⊆ e.target) :
    e.symm '' s = e.source ∩ e ⁻¹' s :=
  e.symm.image_eq_target_inter_inv_preimage h

Inverse Image of Subset Equals Source Intersection with Preimage

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \beta$ such that $s \subseteq e.\text{target}$, the image of $s$ under the inverse partial equivalence $e^{-1}$ equals the intersection of $e.\text{source}$ with the preimage of $s$ under $e$. In symbols: $$ e^{-1}(s) = e.\text{source} \cap e^{-1}(s). $$

PartialEquiv.symm_image_target_inter_eq theorem

(s : Set β) : e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' (e.target ∩ s)

Full source

theorem symm_image_target_inter_eq (s : Set β) :
    e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' (e.target ∩ s) :=
  e.symm.image_source_inter_eq _

Inverse Image of Target Intersection Equals Source Intersection with Preimage

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \beta$, the image of the intersection $e.\text{target} \cap s$ under the inverse function $e^{-1}$ equals the intersection of $e.\text{source}$ with the preimage of $e.\text{target} \cap s$ under $e$. In symbols: $$ e^{-1}(e.\text{target} \cap s) = e.\text{source} \cap e^{-1}(e.\text{target} \cap s). $$

PartialEquiv.symm_image_target_inter_eq' theorem

(s : Set β) : e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' s

Full source

theorem symm_image_target_inter_eq' (s : Set β) : e.symm '' (e.target ∩ s) = e.source ∩ e ⁻¹' s :=
  e.symm.image_source_inter_eq' _

Inverse Image of Target Intersection Equals Source Intersection with Preimage

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \beta$, the image of the intersection $e.\text{target} \cap s$ under the inverse function $e^{-1}$ equals the intersection of $e.\text{source}$ with the preimage of $s$ under $e$. In symbols: $$ e^{-1}(e.\text{target} \cap s) = e.\text{source} \cap e^{-1}(s). $$

PartialEquiv.source_inter_preimage_inv_preimage theorem

(s : Set α) : e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s

Full source

theorem source_inter_preimage_inv_preimage (s : Set α) :
    e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
  Set.ext fun x => and_congr_right_iff.2 fun hx =>
    by simp only [mem_preimage, e.left_inv hx]

Source-Preimage Invariance under Partial Equivalence Inverse

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$, the intersection of the source set $e.\text{source}$ with the preimage of $e^{-1}$'s preimage of $s$ under $e$ is equal to the intersection of $e.\text{source}$ with $s$ itself. In symbols: $$ e.\text{source} \cap e^{-1}(e^{-1}(s)^{-1}) = e.\text{source} \cap s $$

PartialEquiv.source_inter_preimage_target_inter theorem

(s : Set β) : e.source ∩ e ⁻¹' (e.target ∩ s) = e.source ∩ e ⁻¹' s

Full source

theorem source_inter_preimage_target_inter (s : Set β) :
    e.source ∩ e ⁻¹' (e.target ∩ s) = e.source ∩ e ⁻¹' s :=
  ext fun _ => ⟨fun hx => ⟨hx.1, hx.2.2⟩, fun hx => ⟨hx.1, e.map_source hx.1, hx.2⟩⟩

Source-Preimage Intersection Property for Partial Equivalences

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \beta$, the intersection of the source set $e.\text{source}$ with the preimage of $e.\text{target} \cap s$ under $e$ is equal to the intersection of $e.\text{source}$ with the preimage of $s$ under $e$. In symbols: $$ e.\text{source} \cap e^{-1}(e.\text{target} \cap s) = e.\text{source} \cap e^{-1}(s) $$

PartialEquiv.target_inter_inv_preimage_preimage theorem

(s : Set β) : e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s

Full source

theorem target_inter_inv_preimage_preimage (s : Set β) :
    e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
  e.symm.source_inter_preimage_inv_preimage _

Target-Preimage Invariance under Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \beta$, the intersection of the target set $e.\text{target}$ with the preimage of $e$'s preimage of $s$ under $e^{-1}$ is equal to the intersection of $e.\text{target}$ with $s$ itself. In symbols: $$ e.\text{target} \cap e^{-1}(e^{-1}(s)) = e.\text{target} \cap s $$

PartialEquiv.symm_image_image_of_subset_source theorem

{s : Set α} (h : s ⊆ e.source) : e.symm '' (e '' s) = s

Full source

theorem symm_image_image_of_subset_source {s : Set α} (h : s ⊆ e.source) : e.symm '' (e '' s) = s :=
  (e.leftInvOn.mono h).image_image

Inverse Image of Image Equals Original Subset for Partial Equivalences

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$ such that $s \subseteq e.\text{source}$, the image of $e(s)$ under the inverse partial equivalence $e^{-1}$ equals $s$. In symbols: $$ e^{-1}(e(s)) = s $$

PartialEquiv.image_symm_image_of_subset_target theorem

{s : Set β} (h : s ⊆ e.target) : e '' (e.symm '' s) = s

Full source

theorem image_symm_image_of_subset_target {s : Set β} (h : s ⊆ e.target) : e '' (e.symm '' s) = s :=
  e.symm.symm_image_image_of_subset_source h

Image of Inverse Image Equals Original Subset for Partial Equivalences

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \beta$ such that $s \subseteq e.\text{target}$, the image of $e^{-1}(s)$ under $e$ equals $s$. In symbols: $$ e(e^{-1}(s)) = s $$

PartialEquiv.source_subset_preimage_target theorem

: e.source ⊆ e ⁻¹' e.target

Full source

theorem source_subset_preimage_target : e.source ⊆ e ⁻¹' e.target :=
  e.mapsTo

Source Subset of Preimage of Target in Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the source set $e.\text{source} \subseteq \alpha$ is contained in the preimage of the target set $e.\text{target} \subseteq \beta$ under the function $e$, i.e., $e.\text{source} \subseteq e^{-1}(e.\text{target})$.

PartialEquiv.symm_image_target_eq_source theorem

: e.symm '' e.target = e.source

Full source

theorem symm_image_target_eq_source : e.symm '' e.target = e.source :=
  e.symm.image_source_eq_target

Inverse Image of Target Equals Source in Partial Equivalence

Informal description

For a partial equivalence $e$ between types $\alpha$ and $\beta$, the image of the target set $e.\text{target} \subseteq \beta$ under the inverse function $e^{-1}$ equals the source set $e.\text{source} \subseteq \alpha$, i.e., $e^{-1}(e.\text{target}) = e.\text{source}$.

PartialEquiv.target_subset_preimage_source theorem

: e.target ⊆ e.symm ⁻¹' e.source

Full source

theorem target_subset_preimage_source : e.target ⊆ e.symm ⁻¹' e.source :=
  e.symm_mapsTo

Target Subset of Preimage of Source under Inverse Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the target set $e.\text{target} \subseteq \beta$ is contained in the preimage of the source set $e.\text{source} \subseteq \alpha$ under the inverse function $e^{-1}$, i.e., $e.\text{target} \subseteq (e^{-1})^{-1}(e.\text{source})$.

PartialEquiv.ext theorem

 {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x) (hsymm : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) :
  e = e'

Full source

/-- Two partial equivs that have the same `source`, same `toFun` and same `invFun`, coincide. -/
@[ext]
protected theorem ext {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x)
    (hsymm : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e' := by
  have A : (e : α → β) = e' := by
    ext x
    exact h x
  have B : (e.symm : β → α) = e'.symm := by
    ext x
    exact hsymm x
  have I : e '' e.source = e.target := e.image_source_eq_target
  have I' : e' '' e'.source = e'.target := e'.image_source_eq_target
  rw [A, hs, I'] at I
  cases e; cases e'
  simp_all

Equality of Partial Equivalences via Source and Function Agreement

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$. If: 1. The forward maps coincide: $e(x) = e'(x)$ for all $x \in \alpha$, 2. The inverse maps coincide: $e^{-1}(y) = e'^{-1}(y)$ for all $y \in \beta$, 3. The source sets coincide: $e.\text{source} = e'.\text{source}$, then $e = e'$.

PartialEquiv.restr definition

(s : Set α) : PartialEquiv α β

Full source

/-- Restricting a partial equivalence to `e.source ∩ s` -/
protected def restr (s : Set α) : PartialEquiv α β :=
  (@IsImage.of_symm_preimage_eq α β e s (e.symm ⁻¹' s) rfl).restr

Restriction of a partial equivalence to a subset

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$ and a subset $s \subseteq \alpha$, the restriction $e \restriction_s$ is the partial equivalence obtained by: - Restricting the source to $e.\text{source} \cap s$ - Restricting the target to $e.\text{target} \cap e^{-1}(s)$ - Keeping the same forward and inverse functions as $e$ but restricted to these smaller domains This operation preserves the inverse relationship between the functions on their restricted domains.

PartialEquiv.restr_coe theorem

(s : Set α) : (e.restr s : α → β) = e

Full source

@[simp, mfld_simps]
theorem restr_coe (s : Set α) : (e.restr s : α → β) = e :=
  rfl

Restriction Preserves Forward Map: $(e \restriction_s) = e$

Informal description

For any subset $s \subseteq \alpha$, the forward map of the restricted partial equivalence $e \restriction_s$ coincides with the original forward map $e$ on their common domain. That is, $(e \restriction_s)(x) = e(x)$ for all $x \in \alpha$.

PartialEquiv.restr_coe_symm theorem

(s : Set α) : ((e.restr s).symm : β → α) = e.symm

Full source

@[simp, mfld_simps]
theorem restr_coe_symm (s : Set α) : ((e.restr s).symm : β → α) = e.symm :=
  rfl

Inverse Function Preservation under Restriction of Partial Equivalence

Informal description

For any subset $s \subseteq \alpha$, the inverse function of the restricted partial equivalence $e \restriction_s$ is equal to the inverse function of the original partial equivalence $e$ when viewed as functions from $\beta$ to $\alpha$.

PartialEquiv.restr_source theorem

(s : Set α) : (e.restr s).source = e.source ∩ s

Full source

@[simp, mfld_simps]
theorem restr_source (s : Set α) : (e.restr s).source = e.source ∩ s :=
  rfl

Source of Restricted Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$, the source of the restricted partial equivalence $e \restriction s$ is equal to the intersection of the original source $e.\text{source}$ with $s$, i.e., $(e \restriction s).\text{source} = e.\text{source} \cap s$.

PartialEquiv.source_restr_subset_source theorem

(s : Set α) : (e.restr s).source ⊆ e.source

Full source

theorem source_restr_subset_source (s : Set α) : (e.restr s).source ⊆ e.source := inter_subset_left

Source Subset Property under Restriction of Partial Equivalence

Informal description

For any subset $s \subseteq \alpha$, the source of the restricted partial equivalence $e \restriction s$ is a subset of the source of the original partial equivalence $e$, i.e., $(e \restriction s).\text{source} \subseteq e.\text{source}$.

PartialEquiv.restr_target theorem

(s : Set α) : (e.restr s).target = e.target ∩ e.symm ⁻¹' s

Full source

@[simp, mfld_simps]
theorem restr_target (s : Set α) : (e.restr s).target = e.target ∩ e.symm ⁻¹' s :=
  rfl

Target of Restricted Partial Equivalence via Inverse Preimage

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$ and any subset $s \subseteq \alpha$, the target of the restricted partial equivalence $e \restriction s$ is equal to the intersection of the original target $e.\text{target}$ with the preimage of $s$ under the inverse function $e^{-1}$, i.e., $(e \restriction s).\text{target} = e.\text{target} \cap e^{-1}(s)$.

PartialEquiv.restr_eq_of_source_subset theorem

{e : PartialEquiv α β} {s : Set α} (h : e.source ⊆ s) : e.restr s = e

Full source

theorem restr_eq_of_source_subset {e : PartialEquiv α β} {s : Set α} (h : e.source ⊆ s) :
    e.restr s = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [inter_eq_self_of_subset_left h])

Restriction of Partial Equivalence to Superset of Source is Identity

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset containing the source of $e$ (i.e., $e.\text{source} \subseteq s$). Then the restriction of $e$ to $s$ equals $e$ itself.

PartialEquiv.restr_univ theorem

{e : PartialEquiv α β} : e.restr univ = e

Full source

@[simp, mfld_simps]
theorem restr_univ {e : PartialEquiv α β} : e.restr univ = e :=
  restr_eq_of_source_subset (subset_univ _)

Restriction to Universal Set Preserves Partial Equivalence

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the restriction of $e$ to the universal set $\text{univ}$ (the entire type $\alpha$) equals $e$ itself.

PartialEquiv.refl definition

(α : Type*) : PartialEquiv α α

Full source

/-- The identity partial equiv -/
protected def refl (α : Type*) : PartialEquiv α α :=
  (Equiv.refl α).toPartialEquiv

Identity partial equivalence

Informal description

The identity partial equivalence on a type $\alpha$ is the partial equivalence where: - The source and target are both the entire set $\alpha$, - The forward and inverse functions are both the identity function on $\alpha$, - The functions are mutual inverses when restricted to their respective domains.

PartialEquiv.refl_source theorem

: (PartialEquiv.refl α).source = univ

Full source

@[simp, mfld_simps]
theorem refl_source : (PartialEquiv.refl α).source = univ :=
  rfl

Source of Identity Partial Equivalence is Universe

Informal description

The source set of the identity partial equivalence on a type $\alpha$ is the entire set $\alpha$, i.e., $(\text{PartialEquiv.refl } \alpha).\text{source} = \text{univ}$.

PartialEquiv.refl_target theorem

: (PartialEquiv.refl α).target = univ

Full source

@[simp, mfld_simps]
theorem refl_target : (PartialEquiv.refl α).target = univ :=
  rfl

Target of Identity Partial Equivalence is Universe

Informal description

The target set of the identity partial equivalence on a type $\alpha$ is equal to the entire set $\alpha$, i.e., $(\text{PartialEquiv.refl } \alpha).\text{target} = \text{univ}$.

PartialEquiv.refl_coe theorem

: (PartialEquiv.refl α : α → α) = id

Full source

@[simp, mfld_simps]
theorem refl_coe : (PartialEquiv.refl α : α → α) = id :=
  rfl

Identity Partial Equivalence as Identity Function

Informal description

The forward function of the identity partial equivalence on a type $\alpha$ is equal to the identity function on $\alpha$, i.e., $(\text{refl} \alpha)(x) = x$ for all $x \in \alpha$.

PartialEquiv.refl_symm theorem

: (PartialEquiv.refl α).symm = PartialEquiv.refl α

Full source

@[simp, mfld_simps]
theorem refl_symm : (PartialEquiv.refl α).symm = PartialEquiv.refl α :=
  rfl

Inverse of Identity Partial Equivalence is Identity

Informal description

The inverse of the identity partial equivalence on a type $\alpha$ is equal to the identity partial equivalence itself, i.e., $(\text{refl}_{\alpha})^{-1} = \text{refl}_{\alpha}$.

PartialEquiv.refl_restr_source theorem

(s : Set α) : ((PartialEquiv.refl α).restr s).source = s

Full source

@[mfld_simps]
theorem refl_restr_source (s : Set α) : ((PartialEquiv.refl α).restr s).source = s := by simp

Source of Restricted Identity Partial Equivalence

Informal description

For any subset $s$ of a type $\alpha$, the source of the restriction of the identity partial equivalence to $s$ is equal to $s$ itself, i.e., $(\text{refl}_{\alpha} \restriction s).\text{source} = s$.

PartialEquiv.refl_restr_target theorem

(s : Set α) : ((PartialEquiv.refl α).restr s).target = s

Full source

@[mfld_simps]
theorem refl_restr_target (s : Set α) : ((PartialEquiv.refl α).restr s).target = s := by simp

Target of Restricted Identity Partial Equivalence

Informal description

For any subset $s$ of a type $\alpha$, the target of the restriction of the identity partial equivalence to $s$ is equal to $s$ itself. That is, $(\text{refl}_{\alpha} \restriction_s).\text{target} = s$.

PartialEquiv.ofSet definition

(s : Set α) : PartialEquiv α α

Full source

/-- The identity partial equivalence on a set `s` -/
def ofSet (s : Set α) : PartialEquiv α α where
  toFun := id
  invFun := id
  source := s
  target := s
  map_source' _ hx := hx
  map_target' _ hx := hx
  left_inv' _ _ := rfl
  right_inv' _ _ := rfl

Identity Partial Equivalence on a Set

Informal description

The identity partial equivalence on a set $s \subseteq \alpha$ is defined as the partial equivalence where both the source and target are $s$, and the functions are the identity maps on $s$. Specifically: - The source and target are both $s$ - The forward and inverse functions are both the identity function - The functions map elements of $s$ to $s$ (map_source' and map_target') - The functions are inverses of each other when restricted to $s$ (left_inv' and right_inv')

PartialEquiv.ofSet_source theorem

(s : Set α) : (PartialEquiv.ofSet s).source = s

Full source

@[simp, mfld_simps]
theorem ofSet_source (s : Set α) : (PartialEquiv.ofSet s).source = s :=
  rfl

Source of Identity Partial Equivalence on a Set

Informal description

For any subset $s$ of a type $\alpha$, the source of the identity partial equivalence `PartialEquiv.ofSet s` is equal to $s$.

PartialEquiv.ofSet_target theorem

(s : Set α) : (PartialEquiv.ofSet s).target = s

Full source

@[simp, mfld_simps]
theorem ofSet_target (s : Set α) : (PartialEquiv.ofSet s).target = s :=
  rfl

Target of Identity Partial Equivalence on a Set

Informal description

For any subset $s$ of a type $\alpha$, the target of the identity partial equivalence `PartialEquiv.ofSet s` is equal to $s$.

PartialEquiv.ofSet_coe theorem

(s : Set α) : (PartialEquiv.ofSet s : α → α) = id

Full source

@[simp, mfld_simps]
theorem ofSet_coe (s : Set α) : (PartialEquiv.ofSet s : α → α) = id :=
  rfl

Identity Partial Equivalence Function on a Set

Informal description

For any subset $s$ of a type $\alpha$, the function associated with the partial equivalence `PartialEquiv.ofSet s` is equal to the identity function on $\alpha$.

PartialEquiv.ofSet_symm theorem

(s : Set α) : (PartialEquiv.ofSet s).symm = PartialEquiv.ofSet s

Full source

@[simp, mfld_simps]
theorem ofSet_symm (s : Set α) : (PartialEquiv.ofSet s).symm = PartialEquiv.ofSet s :=
  rfl

Inverse of Identity Partial Equivalence on a Set

Informal description

For any subset $s$ of a type $\alpha$, the inverse of the identity partial equivalence on $s$ is equal to itself, i.e., $(\text{PartialEquiv.ofSet } s)^{-1} = \text{PartialEquiv.ofSet } s$.

PartialEquiv.single definition

(a : α) (b : β) : PartialEquiv α β

Full source

/-- `Function.const` as a `PartialEquiv`.
It consists of two constant maps in opposite directions. -/
@[simps]
def single (a : α) (b : β) : PartialEquiv α β where
  toFun := Function.const α b
  invFun := Function.const β a
  source := {a}
  target := {b}
  map_source' _ _ := rfl
  map_target' _ _ := rfl
  left_inv' a' ha' := by rw [eq_of_mem_singleton ha', const_apply]
  right_inv' b' hb' := by rw [eq_of_mem_singleton hb', const_apply]

Singleton Partial Equivalence

Informal description

The partial equivalence `PartialEquiv.single a b` between types $\alpha$ and $\beta$ is defined for a single point $a \in \alpha$ and a single point $b \in \beta$. It consists of two constant functions: the forward function maps every element of $\alpha$ to $b$, and the backward function maps every element of $\beta$ to $a$. The source of this partial equivalence is the singleton set $\{a\}$, and the target is the singleton set $\{b\}$. The functions are inverses of each other when restricted to their respective domains.

PartialEquiv.trans' definition

(e' : PartialEquiv β γ) (h : e.target = e'.source) : PartialEquiv α γ

Full source

/-- Composing two partial equivs if the target of the first coincides with the source of the
second. -/
@[simps]
protected def trans' (e' : PartialEquiv β γ) (h : e.target = e'.source) : PartialEquiv α γ where
  toFun := e' ∘ e
  invFun := e.symm ∘ e'.symm
  source := e.source
  target := e'.target
  map_source' x hx := by simp [← h, hx]
  map_target' y hy := by simp [h, hy]
  left_inv' x hx := by simp [hx, ← h]
  right_inv' y hy := by simp [hy, h]

Composition of Partial Equivalences with Matching Target and Source

Informal description

Given two partial equivalences $e : \alpha \to \beta$ and $e' : \beta \to \gamma$ such that the target of $e$ equals the source of $e'$, the composition $e' \circ e$ is a partial equivalence from $\alpha$ to $\gamma$ defined as follows: - The source is the source of $e$. - The target is the target of $e'$. - The forward function is the composition $e' \circ e$. - The inverse function is the composition $e^{-1} \circ e'^{-1}$. - The functions are inverses of each other when restricted to their respective domains.

PartialEquiv.trans definition

: PartialEquiv α γ

Full source

/-- Composing two partial equivs, by restricting to the maximal domain where their composition
is well defined.
Within the `Manifold` namespace, there is the notation `e ≫ f` for this.
-/
@[trans]
protected def trans : PartialEquiv α γ :=
  PartialEquiv.trans' (e.symm.restr e'.source).symm (e'.restr e.target) (inter_comm _ _)

Composition of partial equivalences

Informal description

The composition of two partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$ is a partial equivalence $e \circ e' : \alpha \rightleftarrows \gamma$ defined by: - The source is $e^{-1}(e.\text{target} \cap e'.\text{source})$ - The target is $e'(e.\text{target} \cap e'.\text{source})$ - The forward function is $e' \circ e$ - The inverse function is $e^{-1} \circ e'^{-1}$ The functions are mutual inverses when restricted to their respective domains. In the `Manifold` namespace, this can be written as $e \gg e'$.

PartialEquiv.coe_trans theorem

: (e.trans e' : α → γ) = e' ∘ e

Full source

@[simp, mfld_simps]
theorem coe_trans : (e.trans e' : α → γ) = e' ∘ e :=
  rfl

Composition of Partial Equivalences as Function Composition

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the forward function of their composition $e \circ e' : \alpha \rightleftarrows \gamma$ is equal to the composition of their forward functions, i.e., $(e \circ e')(x) = e'(e(x))$ for all $x \in \alpha$.

PartialEquiv.coe_trans_symm theorem

: ((e.trans e').symm : γ → α) = e.symm ∘ e'.symm

Full source

@[simp, mfld_simps]
theorem coe_trans_symm : ((e.trans e').symm : γ → α) = e.symm ∘ e'.symm :=
  rfl

Inverse of Composition of Partial Equivalences is Composition of Inverses

Informal description

The inverse of the composition of two partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$ is equal to the composition of their inverses, i.e., $(e \circ e')^{-1} = e^{-1} \circ e'^{-1}$ as functions from $\gamma$ to $\alpha$.

PartialEquiv.trans_apply theorem

{x : α} : (e.trans e') x = e' (e x)

Full source

theorem trans_apply {x : α} : (e.trans e') x = e' (e x) :=
  rfl

Composition of Partial Equivalences at a Point

Informal description

For any element $x$ in the source of the composition $e \circ e'$ of partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the value of the composed function at $x$ is given by $(e \circ e')(x) = e'(e(x))$.

PartialEquiv.trans_symm_eq_symm_trans_symm theorem

: (e.trans e').symm = e'.symm.trans e.symm

Full source

theorem trans_symm_eq_symm_trans_symm : (e.trans e').symm = e'.symm.trans e.symm := by
  cases e; cases e'; rfl

Inverse of Composition Equals Reverse Composition of Inverses for Partial Equivalences

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the inverse of their composition equals the composition of their inverses in reverse order, i.e., $(e \circ e')^{-1} = e'^{-1} \circ e^{-1}$.

PartialEquiv.trans_source theorem

: (e.trans e').source = e.source ∩ e ⁻¹' e'.source

Full source

@[simp, mfld_simps]
theorem trans_source : (e.trans e').source = e.source ∩ e ⁻¹' e'.source :=
  rfl

Source of Composition of Partial Equivalences

Informal description

For two partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the source of their composition $e \circ e'$ is equal to the intersection of the source of $e$ with the preimage under $e$ of the source of $e'$, i.e., $$\text{source}(e \circ e') = \text{source}(e) \cap e^{-1}(\text{source}(e')).$$

PartialEquiv.trans_source' theorem

: (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source)

Full source

theorem trans_source' : (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source) := by
  mfld_set_tac

Source of Composition of Partial Equivalences

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the source of their composition $e \circ e'$ is given by the intersection of the source of $e$ with the preimage under $e$ of the intersection between the target of $e$ and the source of $e'$. In symbols: $$\text{source}(e \circ e') = \text{source}(e) \cap e^{-1}(\text{target}(e) \cap \text{source}(e'))$$

PartialEquiv.trans_source'' theorem

: (e.trans e').source = e.symm '' (e.target ∩ e'.source)

Full source

theorem trans_source'' : (e.trans e').source = e.symm '' (e.target ∩ e'.source) := by
  rw [e.trans_source', e.symm_image_target_inter_eq]

Source of Composition as Inverse Image of Target-Source Intersection

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the source of their composition $e \circ e'$ is equal to the image of the intersection $e.\text{target} \cap e'.\text{source}$ under the inverse function $e^{-1}$. In symbols: $$(e \circ e').\text{source} = e^{-1}(e.\text{target} \cap e'.\text{source}).$$

PartialEquiv.image_trans_source theorem

: e '' (e.trans e').source = e.target ∩ e'.source

Full source

theorem image_trans_source : e '' (e.trans e').source = e.target ∩ e'.source :=
  (e.symm.restr e'.source).symm.image_source_eq_target

Image of Composition's Source Equals Target-Source Intersection

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the image of the source of the composition $e \circ e'$ under $e$ equals the intersection of $e$'s target with $e'$'s source, i.e., $$ e\big((e \circ e').\text{source}\big) = e.\text{target} \cap e'.\text{source}. $$

PartialEquiv.trans_target theorem

: (e.trans e').target = e'.target ∩ e'.symm ⁻¹' e.target

Full source

@[simp, mfld_simps]
theorem trans_target : (e.trans e').target = e'.target ∩ e'.symm ⁻¹' e.target :=
  rfl

Target of Composition of Partial Equivalences

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the target of their composition $e \circ e'$ is equal to the intersection of the target of $e'$ with the preimage of the target of $e$ under the inverse function of $e'$. In symbols: $$(e \circ e').\text{target} = e'.\text{target} \cap (e'^{-1})^{-1}(e.\text{target}).$$

PartialEquiv.trans_target' theorem

: (e.trans e').target = e'.target ∩ e'.symm ⁻¹' (e'.source ∩ e.target)

Full source

theorem trans_target' : (e.trans e').target = e'.target ∩ e'.symm ⁻¹' (e'.source ∩ e.target) :=
  trans_source' e'.symm e.symm

Target of Composition of Partial Equivalences via Preimage of Intersection

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the target of their composition $e \circ e'$ is equal to the intersection of $e'$'s target with the preimage under $e'^{-1}$ of the intersection between $e'$'s source and $e$'s target. That is: $$(e \circ e').\text{target} = e'.\text{target} \cap (e'^{-1})^{-1}(e'.\text{source} \cap e.\text{target}).$$

PartialEquiv.trans_target'' theorem

: (e.trans e').target = e' '' (e'.source ∩ e.target)

Full source

theorem trans_target'' : (e.trans e').target = e' '' (e'.source ∩ e.target) :=
  trans_source'' e'.symm e.symm

Target of Composition as Image of Source-Target Intersection

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the target of their composition $e \circ e'$ is equal to the image of the intersection $e'.\text{source} \cap e.\text{target}$ under the forward function $e'$. In symbols: $$(e \circ e').\text{target} = e'(e'.\text{source} \cap e.\text{target}).$$

PartialEquiv.inv_image_trans_target theorem

: e'.symm '' (e.trans e').target = e'.source ∩ e.target

Full source

theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩ e.target :=
  image_trans_source e'.symm e.symm

Inverse Image of Composition's Target Equals Source-Target Intersection

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, the image of the target of the composition $e \circ e'$ under the inverse of $e'$ equals the intersection of $e'$'s source with $e$'s target, i.e., $$ e'^{-1}\big((e \circ e').\text{target}\big) = e'.\text{source} \cap e.\text{target}. $$

PartialEquiv.trans_assoc theorem

(e'' : PartialEquiv γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'')

Full source

theorem trans_assoc (e'' : PartialEquiv γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'') :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl)
    (by simp [trans_source, @preimage_comp α β γ, inter_assoc])

Associativity of Partial Equivalence Composition

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$, $e' : \beta \rightleftarrows \gamma$, and $e'' : \gamma \rightleftarrows \delta$, the composition operation is associative: $$(e \circ e') \circ e'' = e \circ (e' \circ e'')$$ where $\circ$ denotes the composition of partial equivalences.

PartialEquiv.trans_refl theorem

: e.trans (PartialEquiv.refl β) = e

Full source

@[simp, mfld_simps]
theorem trans_refl : e.trans (PartialEquiv.refl β) = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source])

Right Identity Law for Partial Equivalence Composition

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the composition of $e$ with the identity partial equivalence on $\beta$ is equal to $e$ itself. In other words, $e \circ \text{id}_\beta = e$, where $\text{id}_\beta$ denotes the identity partial equivalence on $\beta$.

PartialEquiv.refl_trans theorem

: (PartialEquiv.refl α).trans e = e

Full source

@[simp, mfld_simps]
theorem refl_trans : (PartialEquiv.refl α).trans e = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source, preimage_id])

Identity Composition Law for Partial Equivalences: $\text{id}_\alpha \circ e = e$

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the composition of the identity partial equivalence on $\alpha$ with $e$ is equal to $e$ itself.

PartialEquiv.trans_ofSet theorem

(s : Set β) : e.trans (ofSet s) = e.restr (e ⁻¹' s)

Full source

theorem trans_ofSet (s : Set β) : e.trans (ofSet s) = e.restr (e ⁻¹' s) :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) rfl

Composition with Identity Partial Equivalence Equals Preimage Restriction

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s \subseteq \beta$ be a subset. The composition of $e$ with the identity partial equivalence on $s$ is equal to the restriction of $e$ to the preimage $e^{-1}(s)$.

PartialEquiv.trans_refl_restr theorem

(s : Set β) : e.trans ((PartialEquiv.refl β).restr s) = e.restr (e ⁻¹' s)

Full source

theorem trans_refl_restr (s : Set β) :
    e.trans ((PartialEquiv.refl β).restr s) = e.restr (e ⁻¹' s) :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source])

Composition with Restricted Identity Equals Preimage Restriction

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s$ be a subset of $\beta$. Then the composition of $e$ with the restriction of the identity partial equivalence on $\beta$ to $s$ is equal to the restriction of $e$ to the preimage $e^{-1}(s)$.

PartialEquiv.trans_refl_restr' theorem

(s : Set β) : e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s)

Full source

theorem trans_refl_restr' (s : Set β) :
    e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s) :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) <| by
    simp only [trans_source, restr_source, refl_source, univ_inter]
    rw [← inter_assoc, inter_self]

Composition with Restricted Identity Equals Restricted Source

Informal description

Let $e$ be a partial equivalence between types $\alpha$ and $\beta$, and let $s$ be a subset of $\beta$. Then the composition of $e$ with the restriction of the identity partial equivalence on $\beta$ to $s$ is equal to the restriction of $e$ to the intersection of its source with the preimage of $s$ under $e$. In symbols: $$ e \circ (\text{id}_\beta \restriction_s) = e \restriction_{e.\text{source} \cap e^{-1}(s)} $$

PartialEquiv.restr_trans theorem

(s : Set α) : (e.restr s).trans e' = (e.trans e').restr s

Full source

theorem restr_trans (s : Set α) : (e.restr s).trans e' = (e.trans e').restr s :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) <| by
    simp [trans_source, inter_comm, inter_assoc]

Restriction-Composition Commutativity for Partial Equivalences

Informal description

Let $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$ be partial equivalences, and let $s \subseteq \alpha$ be a subset. Then the composition of the restriction of $e$ to $s$ with $e'$ is equal to the restriction to $s$ of the composition of $e$ with $e'$. In symbols: $$ (e \restriction_s) \circ e' = (e \circ e') \restriction_s $$

PartialEquiv.mem_symm_trans_source theorem

{e' : PartialEquiv α γ} {x : α} (he : x ∈ e.source) (he' : x ∈ e'.source) : e x ∈ (e.symm.trans e').source

Full source

/-- A lemma commonly useful when `e` and `e'` are charts of a manifold. -/
theorem mem_symm_trans_source {e' : PartialEquiv α γ} {x : α} (he : x ∈ e.source)
    (he' : x ∈ e'.source) : e x ∈ (e.symm.trans e').source :=
  ⟨e.mapsTo he, by rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]⟩

Image under First Chart Belongs to Source of Composed Chart

Informal description

Let $e : \alpha \rightleftarrows \beta$ and $e' : \alpha \rightleftarrows \gamma$ be partial equivalences. For any $x \in \alpha$ that belongs to both the source of $e$ and the source of $e'$, the image $e(x)$ belongs to the source of the composed partial equivalence $e^{-1} \circ e'$.

PartialEquiv.EqOnSource definition

(e e' : PartialEquiv α β) : Prop

Full source

/-- `EqOnSource e e'` means that `e` and `e'` have the same source, and coincide there. Then `e`
and `e'` should really be considered the same partial equiv. -/
def EqOnSource (e e' : PartialEquiv α β) : Prop :=
  e.source = e'.source ∧ e.source.EqOn e e'

Equality on Source for Partial Equivalences

Informal description

Two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$ are said to be equal on source if they have the same source set and coincide on this set. This means $e.\text{source} = e'.\text{source}$ and for all $x \in e.\text{source}$, $e(x) = e'(x)$.

PartialEquiv.eqOnSourceSetoid instance

: Setoid (PartialEquiv α β)

Full source

/-- `EqOnSource` is an equivalence relation. This instance provides the `≈` notation between two
`PartialEquiv`s. -/
instance eqOnSourceSetoid : Setoid (PartialEquiv α β) where
  r := EqOnSource
  iseqv := by constructor <;> simp only [Equivalence, EqOnSource, EqOn] <;> aesop

Equivalence Relation for Partial Equivalences on Source

Informal description

The relation `EqOnSource` defines an equivalence relation on the set of partial equivalences between types $\alpha$ and $\beta$. Two partial equivalences $e$ and $e'$ are equivalent if they have the same source set and coincide on this set.

PartialEquiv.eqOnSource_refl theorem

: e ≈ e

Full source

theorem eqOnSource_refl : e ≈ e :=
  Setoid.refl _

Reflexivity of Partial Equivalence Equality on Source

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the relation $\approx$ (equality on source) is reflexive, i.e., $e \approx e$.

PartialEquiv.EqOnSource.source_eq theorem

{e e' : PartialEquiv α β} (h : e ≈ e') : e.source = e'.source

Full source

/-- Two equivalent partial equivs have the same source. -/
theorem EqOnSource.source_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.source = e'.source :=
  h.1

Equality of Source Sets for Equivalent Partial Equivalences

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e$ and $e'$ are equivalent under the relation $\approx$ (i.e., they have the same source and coincide on this source), then their source sets are equal: $e.\text{source} = e'.\text{source}$.

PartialEquiv.EqOnSource.eqOn theorem

{e e' : PartialEquiv α β} (h : e ≈ e') : e.source.EqOn e e'

Full source

/-- Two equivalent partial equivs coincide on the source. -/
theorem EqOnSource.eqOn {e e' : PartialEquiv α β} (h : e ≈ e') : e.source.EqOn e e' :=
  h.2

Coincidence of Equivalent Partial Equivalences on Source

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e \approx e'$ (i.e., they are equivalent under the `EqOnSource` relation), then $e$ and $e'$ coincide on their common source set $e.\text{source} = e'.\text{source}$.

PartialEquiv.EqOnSource.target_eq theorem

{e e' : PartialEquiv α β} (h : e ≈ e') : e.target = e'.target

Full source

/-- Two equivalent partial equivs have the same target. -/
theorem EqOnSource.target_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.target = e'.target := by
  simp only [← image_source_eq_target, ← source_eq h, h.2.image_eq]

Equality of Target Sets for Equivalent Partial Equivalences

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e \approx e'$ (i.e., they are equivalent under the `EqOnSource` relation), then their target sets are equal: $e.\text{target} = e'.\text{target}$.

PartialEquiv.EqOnSource.symm' theorem

{e e' : PartialEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm

Full source

/-- If two partial equivs are equivalent, so are their inverses. -/
theorem EqOnSource.symm' {e e' : PartialEquiv α β} (h : e ≈ e') : e.symm ≈ e'.symm := by
  refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩ <;>
    simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
  exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)

Equivalence of Inverses for Equivalent Partial Equivalences

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e$ and $e'$ are equivalent under the relation $\approx$ (i.e., they have the same source set and coincide on this set), then their inverse partial equivalences $e^{-1}$ and $e'^{-1}$ are also equivalent under $\approx$.

PartialEquiv.EqOnSource.symm_eqOn theorem

{e e' : PartialEquiv α β} (h : e ≈ e') : EqOn e.symm e'.symm e.target

Full source

/-- Two equivalent partial equivs have coinciding inverses on the target. -/
theorem EqOnSource.symm_eqOn {e e' : PartialEquiv α β} (h : e ≈ e') :
    EqOn e.symm e'.symm e.target :=
  -- Porting note: `h.symm'` dot notation doesn't work anymore because `h` is not recognised as
  -- `PartialEquiv.EqOnSource` for some reason.
  eqOn (symm' h)

Inverse Functions Coincide on Target for Equivalent Partial Equivalences

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e$ and $e'$ are equivalent under the relation $\approx$ (i.e., they have the same source set and coincide on this set), then their inverse functions $e^{-1}$ and $e'^{-1}$ coincide on the target set $e.\text{target} = e'.\text{target}$.

PartialEquiv.EqOnSource.trans' theorem

{e e' : PartialEquiv α β} {f f' : PartialEquiv β γ} (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f'

Full source

/-- Composition of partial equivs respects equivalence. -/
theorem EqOnSource.trans' {e e' : PartialEquiv α β} {f f' : PartialEquiv β γ} (he : e ≈ e')
    (hf : f ≈ f') : e.trans f ≈ e'.trans f' := by
  constructor
  · rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]
    exact (he.symm'.eqOn.mono inter_subset_left).image_eq
  · intro x hx
    rw [trans_source] at hx
    simp [Function.comp_apply, PartialEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]

Composition Preserves Partial Equivalence Relation

Informal description

Let $e, e' : \alpha \rightleftarrows \beta$ and $f, f' : \beta \rightleftarrows \gamma$ be partial equivalences such that $e \approx e'$ and $f \approx f'$ under the `EqOnSource` equivalence relation. Then the composition of partial equivalences satisfies $e \circ f \approx e' \circ f'$. Here, $e \approx e'$ means that $e$ and $e'$ have the same source set and coincide on this set, and similarly for $f \approx f'$.

PartialEquiv.EqOnSource.restr theorem

{e e' : PartialEquiv α β} (he : e ≈ e') (s : Set α) : e.restr s ≈ e'.restr s

Full source

/-- Restriction of partial equivs respects equivalence. -/
theorem EqOnSource.restr {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set α) :
    e.restr s ≈ e'.restr s := by
  constructor
  · simp [he.1]
  · intro x hx
    simp only [mem_inter_iff, restr_source] at hx
    exact he.2 hx.1

Restriction Preserves Partial Equivalence Relation

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e$ and $e'$ are equivalent under the relation $\approx$ (i.e., they have the same source set and coincide on this set), then for any subset $s \subseteq \alpha$, the restrictions $e \restriction_s$ and $e' \restriction_s$ are also equivalent under $\approx$.

PartialEquiv.EqOnSource.source_inter_preimage_eq theorem

{e e' : PartialEquiv α β} (he : e ≈ e') (s : Set β) : e.source ∩ e ⁻¹' s = e'.source ∩ e' ⁻¹' s

Full source

/-- Preimages are respected by equivalence. -/
theorem EqOnSource.source_inter_preimage_eq {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set β) :
    e.source ∩ e ⁻¹' s = e'.source ∩ e' ⁻¹' s := by rw [he.eqOn.inter_preimage_eq, source_eq he]

Equality of Source-Preimage Intersections for Equivalent Partial Equivalences

Informal description

For any two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, if $e \approx e'$ (i.e., they are equivalent under the `EqOnSource` relation), then for any subset $s \subseteq \beta$, the intersection of the source set of $e$ with the preimage of $s$ under $e$ is equal to the intersection of the source set of $e'$ with the preimage of $s$ under $e'$. In other words: $$ e.\text{source} \cap e^{-1}(s) = e'.\text{source} \cap e'^{-1}(s). $$

PartialEquiv.self_trans_symm theorem

: e.trans e.symm ≈ ofSet e.source

Full source

/-- Composition of a partial equivalence and its inverse is equivalent to
the restriction of the identity to the source. -/
theorem self_trans_symm : e.trans e.symm ≈ ofSet e.source := by
  have A : (e.trans e.symm).source = e.source := by mfld_set_tac
  refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩
  rw [A] at hx
  simp only [hx, mfld_simps]

Composition of Partial Equivalence with its Inverse is Identity on Source

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the composition $e \circ e^{-1}$ is equivalent to the identity partial equivalence restricted to the source set $e.\text{source}$ of $e$.

PartialEquiv.symm_trans_self theorem

: e.symm.trans e ≈ ofSet e.target

Full source

/-- Composition of the inverse of a partial equivalence and this partial equivalence is equivalent
to the restriction of the identity to the target. -/
theorem symm_trans_self : e.symm.trans e ≈ ofSet e.target :=
  self_trans_symm e.symm

Inverse-Precomposition Yields Identity on Target

Informal description

For any partial equivalence $e$ between types $\alpha$ and $\beta$, the composition of its inverse $e^{-1}$ with $e$ is equivalent to the identity partial equivalence restricted to the target set $e.\text{target}$ of $e$.

PartialEquiv.prod definition

(e : PartialEquiv α β) (e' : PartialEquiv γ δ) : PartialEquiv (α × γ) (β × δ)

Full source

/-- The product of two partial equivalences, as a partial equivalence on the product. -/
def prod (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : PartialEquiv (α × γ) (β × δ) where
  source := e.source ×ˢ e'.source
  target := e.target ×ˢ e'.target
  toFun p := (e p.1, e' p.2)
  invFun p := (e.symm p.1, e'.symm p.2)
  map_source' p hp := by simp_all
  map_target' p hp := by simp_all
  left_inv' p hp   := by simp_all
  right_inv' p hp  := by simp_all

Product of partial equivalences

Informal description

Given partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \gamma \rightleftarrows \delta$, their product $e \times e'$ is a partial equivalence between $\alpha \times \gamma$ and $\beta \times \delta$ defined by: - The source is the product $e.\text{source} \times e'.\text{source}$, - The target is the product $e.\text{target} \times e'.\text{target}$, - The forward map sends $(x, y)$ to $(e(x), e'(y))$, - The inverse map sends $(u, v)$ to $(e^{-1}(u), e'^{-1}(v))$. This construction ensures that $e \times e'$ is indeed a partial equivalence, with the expected inverse relationship.

PartialEquiv.prod_source theorem

(e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.prod e').source = e.source ×ˢ e'.source

Full source

@[simp, mfld_simps]
theorem prod_source (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    (e.prod e').source = e.source ×ˢ e'.source :=
  rfl

Source of Product Partial Equivalence is Product of Sources

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \gamma \rightleftarrows \delta$, the source of their product partial equivalence $e \times e'$ is equal to the product of their sources, i.e., $(e \times e').\text{source} = e.\text{source} \times e'.\text{source}$.

PartialEquiv.prod_target theorem

(e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.prod e').target = e.target ×ˢ e'.target

Full source

@[simp, mfld_simps]
theorem prod_target (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    (e.prod e').target = e.target ×ˢ e'.target :=
  rfl

Target of Product of Partial Equivalences is Product of Targets

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \gamma \rightleftarrows \delta$, the target of their product $e \times e'$ is the Cartesian product of their individual targets, i.e., $(e \times e').\text{target} = e.\text{target} \times e'.\text{target}$.

PartialEquiv.prod_coe theorem

(e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.prod e' : α × γ → β × δ) = fun p => (e p.1, e' p.2)

Full source

@[simp, mfld_simps]
theorem prod_coe (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    (e.prod e' : α × γ → β × δ) = fun p => (e p.1, e' p.2) :=
  rfl

Forward Map of Product Partial Equivalence

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \gamma \rightleftarrows \delta$, the forward map of their product $e \times e'$ is given by $(e \times e')(x, y) = (e(x), e'(y))$ for all $(x, y) \in \alpha \times \gamma$.

PartialEquiv.prod_coe_symm theorem

 (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
  ((e.prod e').symm : β × δ → α × γ) = fun p => (e.symm p.1, e'.symm p.2)

Full source

theorem prod_coe_symm (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    ((e.prod e').symm : β × δ → α × γ) = fun p => (e.symm p.1, e'.symm p.2) :=
  rfl

Inverse of Product of Partial Equivalences

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \gamma \rightleftarrows \delta$, the inverse function of their product $e \times e'$ is given by $(e \times e')^{-1}(u, v) = (e^{-1}(u), e'^{-1}(v))$ for all $(u, v) \in \beta \times \delta$.

PartialEquiv.prod_symm theorem

(e : PartialEquiv α β) (e' : PartialEquiv γ δ) : (e.prod e').symm = e.symm.prod e'.symm

Full source

@[simp, mfld_simps]
theorem prod_symm (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
    (e.prod e').symm = e.symm.prod e'.symm := by
  ext x <;> simp [prod_coe_symm]

Inverse of Product of Partial Equivalences is Product of Inverses

Informal description

For any partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \gamma \rightleftarrows \delta$, the inverse of their product $e \times e'$ is equal to the product of their inverses $e^{-1} \times e'^{-1}$.

PartialEquiv.refl_prod_refl theorem

: (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)

Full source

@[simp, mfld_simps]
theorem refl_prod_refl :
    (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β) := by
  ext ⟨x, y⟩ <;> simp

Product of Identity Partial Equivalences is Identity on Product Space

Informal description

The product of the identity partial equivalences on types $\alpha$ and $\beta$ is equal to the identity partial equivalence on the product type $\alpha \times \beta$.

PartialEquiv.prod_trans theorem

 {η : Type*} {ε : Type*} (e : PartialEquiv α β) (f : PartialEquiv β γ) (e' : PartialEquiv δ η) (f' : PartialEquiv η ε) :
  (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Full source

@[simp, mfld_simps]
theorem prod_trans {η : Type*} {ε : Type*} (e : PartialEquiv α β) (f : PartialEquiv β γ)
    (e' : PartialEquiv δ η) (f' : PartialEquiv η ε) :
    (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') := by
  ext ⟨x, y⟩ <;> simp [Set.ext_iff]; tauto

Composition of Product Partial Equivalences Equals Product of Compositions

Informal description

Let $e : \alpha \rightleftarrows \beta$, $f : \beta \rightleftarrows \gamma$, $e' : \delta \rightleftarrows \eta$, and $f' : \eta \rightleftarrows \varepsilon$ be partial equivalences. Then the composition of the product partial equivalences $(e \times e') \circ (f \times f')$ is equal to the product of the compositions $(e \circ f) \times (e' \circ f')$.

PartialEquiv.piecewise definition

 (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [∀ x, Decidable (x ∈ s)] [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t)
  (H' : e'.IsImage s t) : PartialEquiv α β

Full source

/-- Combine two `PartialEquiv`s using `Set.piecewise`. The source of the new `PartialEquiv` is
`s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s`, and similarly for target.  The function
sends `e.source ∩ s` to `e.target ∩ t` using `e` and `e'.source \ s` to `e'.target \ t` using `e'`,
and similarly for the inverse function. The definition assumes `e.isImage s t` and
`e'.isImage s t`. -/
@[simps -fullyApplied]
def piecewise (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [∀ x, Decidable (x ∈ s)]
    [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
    PartialEquiv α β where
  toFun := s.piecewise e e'
  invFun := t.piecewise e.symm e'.symm
  source := s.ite e.source e'.source
  target := t.ite e.target e'.target
  map_source' := H.mapsTo.piecewise_ite H'.compl.mapsTo
  map_target' := H.symm.mapsTo.piecewise_ite H'.symm.compl.mapsTo
  left_inv' := H.leftInvOn_piecewise H'
  right_inv' := H.symm.leftInvOn_piecewise H'.symm

Piecewise-defined partial equivalence

Informal description

Given two partial equivalences $e$ and $e'$ between types $\alpha$ and $\beta$, subsets $s \subseteq \alpha$ and $t \subseteq \beta$ such that $t$ is the image of $s$ under both $e$ and $e'$, the partial equivalence $e.piecewise\ e'\ s\ t$ is defined as follows: - The forward function is $e$ on $s$ and $e'$ on its complement. - The inverse function is $e^{-1}$ on $t$ and $e'^{-1}$ on its complement. - The source is $e.source$ on $s$ and $e'.source$ on its complement. - The target is $e.target$ on $t$ and $e'.target$ on its complement. This construction ensures that the resulting partial equivalence is well-defined and maintains the inverse relationship between the functions on their respective domains.

PartialEquiv.symm_piecewise theorem

 (e e' : PartialEquiv α β) {s : Set α} {t : Set β} [∀ x, Decidable (x ∈ s)] [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t)
  (H' : e'.IsImage s t) : (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm

Full source

theorem symm_piecewise (e e' : PartialEquiv α β) {s : Set α} {t : Set β} [∀ x, Decidable (x ∈ s)]
    [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
    (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm :=
  rfl

Inverse of Piecewise Partial Equivalence

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$, with subsets $s \subseteq \alpha$ and $t \subseteq \beta$ such that $t$ is the image of $s$ under both $e$ and $e'$ (i.e., $e.\text{IsImage}\ s\ t$ and $e'.\text{IsImage}\ s\ t$ hold). Then the inverse of the piecewise-defined partial equivalence $e.piecewise\ e'\ s\ t$ is equal to the piecewise-defined partial equivalence formed by the inverses $e^{-1}$ and $e'^{-1}$ with domains $t$ and $s$ respectively, i.e., $$(e.piecewise\ e'\ s\ t)^{-1} = e^{-1}.piecewise\ e'^{-1}\ t\ s.$$

PartialEquiv.disjointUnion definition

 (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target)
  [∀ x, Decidable (x ∈ e.source)] [∀ y, Decidable (y ∈ e.target)] : PartialEquiv α β

Full source

/-- Combine two `PartialEquiv`s with disjoint sources and disjoint targets. We reuse
`PartialEquiv.piecewise`, then override `source` and `target` to ensure better definitional
equalities. -/
@[simps! -fullyApplied]
def disjointUnion (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
    (ht : Disjoint e.target e'.target) [∀ x, Decidable (x ∈ e.source)]
    [∀ y, Decidable (y ∈ e.target)] : PartialEquiv α β :=
  (e.piecewise e' e.source e.target e.isImage_source_target <|
        e'.isImage_source_target_of_disjoint _ hs.symm ht.symm).copy
    _ rfl _ rfl (e.source ∪ e'.source) (ite_left _ _) (e.target ∪ e'.target) (ite_left _ _)

Disjoint union of partial equivalences

Informal description

Given two partial equivalences $ e $ and $ e' $ between types $ \alpha $ and $ \beta $ with disjoint sources $ e.\text{source} \cap e'.\text{source} = \emptyset $ and disjoint targets $ e.\text{target} \cap e'.\text{target} = \emptyset $, the disjoint union $ e \sqcup e' $ is a partial equivalence defined by: - The source is the union $ e.\text{source} \cup e'.\text{source} $, - The target is the union $ e.\text{target} \cup e'.\text{target} $, - The forward function is $ e $ on $ e.\text{source} $ and $ e' $ on $ e'.\text{source} $, - The inverse function is $ e^{-1} $ on $ e.\text{target} $ and $ e'^{-1} $ on $ e'.\text{target} $. This construction ensures that the resulting partial equivalence is well-defined and maintains the inverse relationship between the functions on their respective domains.

PartialEquiv.disjointUnion_eq_piecewise theorem

 (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target)
  [∀ x, Decidable (x ∈ e.source)] [∀ y, Decidable (y ∈ e.target)] :
  e.disjointUnion e' hs ht =
    e.piecewise e' e.source e.target e.isImage_source_target (e'.isImage_source_target_of_disjoint _ hs.symm ht.symm)

Full source

theorem disjointUnion_eq_piecewise (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
    (ht : Disjoint e.target e'.target) [∀ x, Decidable (x ∈ e.source)]
    [∀ y, Decidable (y ∈ e.target)] :
    e.disjointUnion e' hs ht =
      e.piecewise e' e.source e.target e.isImage_source_target
        (e'.isImage_source_target_of_disjoint _ hs.symm ht.symm) :=
  copy_eq ..

Disjoint Union of Partial Equivalences Equals Piecewise Construction

Informal description

Let $e$ and $e'$ be partial equivalences between types $\alpha$ and $\beta$ with disjoint sources ($e.\text{source} \cap e'.\text{source} = \emptyset$) and disjoint targets ($e.\text{target} \cap e'.\text{target} = \emptyset$). Then the disjoint union $e \sqcup e'$ is equal to the piecewise-defined partial equivalence constructed by: - Using $e$ on its source $e.\text{source}$ and target $e.\text{target}$, - Using $e'$ on the complement of $e.\text{source}$ and $e.\text{target}$, where $e.\text{target}$ is the image of $e.\text{source}$ under $e$, and $e'.\text{target}$ is the image of $e'.\text{source}$ under $e'$ (with the roles reversed due to disjointness).

PartialEquiv.pi definition

(ei : ∀ i, PartialEquiv (αi i) (βi i)) : PartialEquiv (∀ i, αi i) (∀ i, βi i)

Full source

/-- The product of a family of partial equivalences, as a partial equivalence on the pi type. -/
@[simps (config := mfld_cfg) apply source target]
protected def pi (ei : ∀ i, PartialEquiv (αi i) (βi i)) : PartialEquiv (∀ i, αi i) (∀ i, βi i) where
  toFun := Pi.map fun i ↦ ei i
  invFun := Pi.map fun i ↦ (ei i).symm
  source := pi univ fun i => (ei i).source
  target := pi univ fun i => (ei i).target
  map_source' _ hf i hi := (ei i).map_source (hf i hi)
  map_target' _ hf i hi := (ei i).map_target (hf i hi)
  left_inv' _ hf := funext fun i => (ei i).left_inv (hf i trivial)
  right_inv' _ hf := funext fun i => (ei i).right_inv (hf i trivial)

Product of Partial Equivalences

Informal description

Given a family of partial equivalences $ e_i $ between types $ \alpha_i $ and $ \beta_i $ for each $ i $ in some index set, the product partial equivalence $ \prod_i e_i $ is defined between the product types $ \prod_i \alpha_i $ and $ \prod_i \beta_i $. Specifically: - The source of $ \prod_i e_i $ is the set of all functions $ f $ in $ \prod_i \alpha_i $ such that for each $ i $, $ f(i) $ belongs to the source of $ e_i $. - The target of $ \prod_i e_i $ is the set of all functions $ g $ in $ \prod_i \beta_i $ such that for each $ i $, $ g(i) $ belongs to the target of $ e_i $. - The forward function $ \text{toFun} $ of $ \prod_i e_i $ maps a function $ f $ to the function $ \lambda i, e_i(f(i)) $. - The inverse function $ \text{invFun} $ of $ \prod_i e_i $ maps a function $ g $ to the function $ \lambda i, e_i^{-1}(g(i)) $. The partial equivalence $ \prod_i e_i $ satisfies the following properties: 1. If $ f $ is in the source, then $ e_i(f(i)) $ is in the target of $ e_i $ for each $ i $. 2. If $ g $ is in the target, then $ e_i^{-1}(g(i)) $ is in the source of $ e_i $ for each $ i $. 3. For any $ f $ in the source, applying the forward and then the inverse function returns $ f $ (i.e., $ e_i^{-1}(e_i(f(i))) = f(i) $ for all $ i $). 4. For any $ g $ in the target, applying the inverse and then the forward function returns $ g $ (i.e., $ e_i(e_i^{-1}(g(i))) = g(i) $ for all $ i $).

PartialEquiv.pi_symm theorem

(ei : ∀ i, PartialEquiv (αi i) (βi i)) : (PartialEquiv.pi ei).symm = .pi fun i ↦ (ei i).symm

Full source

@[simp, mfld_simps]
theorem pi_symm (ei : ∀ i, PartialEquiv (αi i) (βi i)) :
    (PartialEquiv.pi ei).symm = .pi fun i ↦ (ei i).symm :=
  rfl

Inverse of Product of Partial Equivalences is Product of Inverses

Informal description

Given a family of partial equivalences $ e_i $ between types $ \alpha_i $ and $ \beta_i $ for each index $ i $, the inverse of the product partial equivalence $ \prod_i e_i $ is equal to the product of the inverses $ \prod_i e_i^{-1} $. In other words, $ \left(\prod_i e_i\right)^{-1} = \prod_i e_i^{-1} $.

PartialEquiv.pi_symm_apply theorem

(ei : ∀ i, PartialEquiv (αi i) (βi i)) : ⇑(PartialEquiv.pi ei).symm = fun f i ↦ (ei i).symm (f i)

Full source

theorem pi_symm_apply (ei : ∀ i, PartialEquiv (αi i) (βi i)) :
    ⇑(PartialEquiv.pi ei).symm = fun f i ↦ (ei i).symm (f i) :=
  rfl

Inverse of Product Partial Equivalence Acts Componentwise

Informal description

For a family of partial equivalences $ e_i $ between types $ \alpha_i $ and $ \beta_i $ indexed by $ i $, the inverse of the product partial equivalence $ \prod_i e_i $ is given by the function $ f \mapsto \lambda i, (e_i)^{-1}(f(i)) $. In other words, the inverse function of the product equivalence acts componentwise by applying the inverse of each $ e_i $ to the corresponding component of $ f $.

PartialEquiv.pi_refl theorem

: (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) = .refl (∀ i, αi i)

Full source

@[simp, mfld_simps]
theorem pi_refl : (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) = .refl (∀ i, αi i) := by
  ext <;> simp

Product of Identity Partial Equivalences is Identity on Product Type

Informal description

For any family of types $\alpha_i$ indexed by $i$, the product of the identity partial equivalences on each $\alpha_i$ is equal to the identity partial equivalence on the product type $\prod_i \alpha_i$. In other words, $\prod_i \text{id}_{\alpha_i} = \text{id}_{\prod_i \alpha_i}$.

PartialEquiv.pi_trans theorem

 (ei : ∀ i, PartialEquiv (αi i) (βi i)) (ei' : ∀ i, PartialEquiv (βi i) (γi i)) :
  (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = .pi fun i ↦ (ei i).trans (ei' i)

Full source

@[simp, mfld_simps]
theorem pi_trans (ei : ∀ i, PartialEquiv (αi i) (βi i)) (ei' : ∀ i, PartialEquiv (βi i) (γi i)) :
    (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = .pi fun i ↦ (ei i).trans (ei' i) := by
  ext <;> simp [forall_and]

Composition of Product Partial Equivalences is Componentwise

Informal description

For any family of partial equivalences $ e_i : \alpha_i \rightleftarrows \beta_i $ and $ e'_i : \beta_i \rightleftarrows \gamma_i $ indexed by $ i $, the composition of the product partial equivalences $ \prod_i e_i $ and $ \prod_i e'_i $ is equal to the product of the componentwise compositions $ \prod_i (e_i \circ e'_i) $. In other words, \[ \left(\prod_i e_i\right) \circ \left(\prod_i e'_i\right) = \prod_i (e_i \circ e'_i). \]

Set.BijOn.toPartialEquiv definition

[Nonempty α] (f : α → β) (s : Set α) (t : Set β) (hf : BijOn f s t) : PartialEquiv α β

Full source

/-- A bijection between two sets `s : Set α` and `t : Set β` provides a partial equivalence
between `α` and `β`. -/
@[simps -fullyApplied]
noncomputable def BijOn.toPartialEquiv [Nonempty α] (f : α → β) (s : Set α) (t : Set β)
    (hf : BijOn f s t) : PartialEquiv α β where
  toFun := f
  invFun := invFunOn f s
  source := s
  target := t
  map_source' := hf.mapsTo
  map_target' := hf.surjOn.mapsTo_invFunOn
  left_inv' := hf.invOn_invFunOn.1
  right_inv' := hf.invOn_invFunOn.2

Partial equivalence from a bijection between subsets

Informal description

Given a nonempty type $\alpha$, a function $f : \alpha \to \beta$, subsets $s \subseteq \alpha$ and $t \subseteq \beta$, and a proof that $f$ is a bijection from $s$ to $t$, this constructs a partial equivalence between $\alpha$ and $\beta$ with source $s$ and target $t$. The forward map is $f$ and the inverse map is the restriction of the inverse function of $f$ to $s$. More precisely: - The forward map is $f$ restricted to $s$ - The inverse map is the function that maps each $y \in t$ to its unique preimage in $s$ under $f$ - The source is exactly $s$ - The target is exactly $t$ - The maps are inverses of each other when restricted to their respective domains

Set.InjOn.toPartialEquiv definition

[Nonempty α] (f : α → β) (s : Set α) (hf : InjOn f s) : PartialEquiv α β

Full source

/-- A map injective on a subset of its domain provides a partial equivalence. -/
@[simp, mfld_simps]
noncomputable def InjOn.toPartialEquiv [Nonempty α] (f : α → β) (s : Set α) (hf : InjOn f s) :
    PartialEquiv α β :=
  hf.bijOn_image.toPartialEquiv f s (f '' s)

Partial equivalence from an injective function on a subset

Informal description

Given a nonempty type $\alpha$, a function $f : \alpha \to \beta$, a subset $s \subseteq \alpha$, and a proof that $f$ is injective on $s$, this constructs a partial equivalence between $\alpha$ and $\beta$ with source $s$ and target $f(s)$. The forward map is $f$ restricted to $s$ and the inverse map is the function that maps each $y \in f(s)$ to its unique preimage in $s$ under $f$. More precisely: - The forward map is $f$ restricted to $s$ - The inverse map is the function that maps each $y \in f(s)$ to its unique preimage in $s$ under $f$ - The source is exactly $s$ - The target is exactly $f(s)$ - The maps are inverses of each other when restricted to their respective domains

Equiv.refl_toPartialEquiv theorem

: (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α

Full source

@[simp, mfld_simps]
theorem refl_toPartialEquiv : (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α :=
  rfl

Identity Equivalence Yields Identity Partial Equivalence

Informal description

The partial equivalence obtained from the identity equivalence on a type $\alpha$ is equal to the identity partial equivalence on $\alpha$.

Equiv.symm_toPartialEquiv theorem

: e.symm.toPartialEquiv = e.toPartialEquiv.symm

Full source

@[simp, mfld_simps]
theorem symm_toPartialEquiv : e.symm.toPartialEquiv = e.toPartialEquiv.symm :=
  rfl

Inverse of Partial Equivalence from Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$, the partial equivalence obtained from its inverse $e^{-1}$ is equal to the inverse of the partial equivalence obtained from $e$. In other words, $(e^{-1}).\text{toPartialEquiv} = (e.\text{toPartialEquiv})^{-1}$.

Equiv.trans_toPartialEquiv theorem

: (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv

Full source

@[simp, mfld_simps]
theorem trans_toPartialEquiv :
    (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl)
    (by simp [PartialEquiv.trans_source, Equiv.toPartialEquiv])

Compatibility of Partial Equivalence Construction with Composition of Equivalences

Informal description

For any equivalences $e : \alpha \simeq \beta$ and $e' : \beta \simeq \gamma$, the partial equivalence obtained from their composition $e \circ e'$ is equal to the composition of the partial equivalences obtained from $e$ and $e'$. That is, $(e \circ e').\text{toPartialEquiv} = e.\text{toPartialEquiv} \circ e'.\text{toPartialEquiv}$.

Equiv.transPartialEquiv definition

(e : α ≃ β) (f' : PartialEquiv β γ) : PartialEquiv α γ

Full source

/-- Precompose a partial equivalence with an equivalence.
We modify the source and target to have better definitional behavior. -/
@[simps!]
def transPartialEquiv (e : α ≃ β) (f' : PartialEquiv β γ) : PartialEquiv α γ :=
  (e.toPartialEquiv.trans f').copy _ rfl _ rfl (e ⁻¹' f'.source) (univ_inter _) f'.target
    (inter_univ _)

Composition of equivalence with partial equivalence

Informal description

Given a bijective map $e : \alpha \simeq \beta$ and a partial equivalence $f'$ from $\beta$ to $\gamma$, the composition $e \circ f'$ is a partial equivalence from $\alpha$ to $\gamma$ defined by: - The source is the preimage of $f'$'s source under $e$ (i.e., $e^{-1}(f'.\text{source})$) - The target is $f'$'s target - The forward function is $f' \circ e$ - The inverse function is $e^{-1} \circ f'^{-1}$ The functions are mutual inverses when restricted to their respective domains.

Equiv.transPartialEquiv_eq_trans theorem

(e : α ≃ β) (f' : PartialEquiv β γ) : e.transPartialEquiv f' = e.toPartialEquiv.trans f'

Full source

theorem transPartialEquiv_eq_trans (e : α ≃ β) (f' : PartialEquiv β γ) :
    e.transPartialEquiv f' = e.toPartialEquiv.trans f' :=
  PartialEquiv.copy_eq ..

Equality of Partial Equivalence Compositions: $e \circ_{\text{partial}} f' = e.\text{toPartialEquiv} \circ f'$

Informal description

For any equivalence (bijection) $e : \alpha \simeq \beta$ and any partial equivalence $f'$ from $\beta$ to $\gamma$, the composition of $e$ with $f'$ as a partial equivalence is equal to the composition of the partial equivalence version of $e$ with $f'$. That is, $e \circ_{\text{partial}} f' = e.\text{toPartialEquiv} \circ f'$.

Equiv.transPartialEquiv_trans theorem

 (e : α ≃ β) (f' : PartialEquiv β γ) (f'' : PartialEquiv γ δ) :
  (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')

Full source

@[simp, mfld_simps]
theorem transPartialEquiv_trans (e : α ≃ β) (f' : PartialEquiv β γ) (f'' : PartialEquiv γ δ) :
    (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'') := by
  simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc]

Associativity of Partial Equivalence Composition via Equivalence

Informal description

For any equivalence (bijection) $e : \alpha \simeq \beta$ and any partial equivalences $f' : \beta \rightleftarrows \gamma$ and $f'' : \gamma \rightleftarrows \delta$, the following equality holds: $$(e \circ_{\text{partial}} f') \circ_{\text{partial}} f'' = e \circ_{\text{partial}} (f' \circ_{\text{partial}} f'')$$ where $\circ_{\text{partial}}$ denotes the composition of partial equivalences.

Equiv.trans_transPartialEquiv theorem

 (e : α ≃ β) (e' : β ≃ γ) (f'' : PartialEquiv γ δ) :
  (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')

Full source

@[simp, mfld_simps]
theorem trans_transPartialEquiv (e : α ≃ β) (e' : β ≃ γ) (f'' : PartialEquiv γ δ) :
    (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'') := by
  simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc, trans_toPartialEquiv]

Associativity of Partial Equivalence Composition with Full Equivalences

Informal description

For any equivalences $e : \alpha \simeq \beta$ and $e' : \beta \simeq \gamma$, and any partial equivalence $f'' : \gamma \rightleftarrows \delta$, the following equality holds: $$(e \circ e') \circ_{\text{partial}} f'' = e \circ_{\text{partial}} (e' \circ_{\text{partial}} f'')$$ where $\circ$ denotes composition of equivalences and $\circ_{\text{partial}}$ denotes composition with a partial equivalence.

PartialEquiv.transEquiv definition

(e : PartialEquiv α β) (f' : β ≃ γ) : PartialEquiv α γ

Full source

/-- Postcompose a partial equivalence with an equivalence.
We modify the source and target to have better definitional behavior. -/
@[simps!]
def transEquiv (e : PartialEquiv α β) (f' : β ≃ γ) : PartialEquiv α γ :=
  (e.trans f'.toPartialEquiv).copy _ rfl _ rfl e.source (inter_univ _) (f'.symm ⁻¹' e.target)
    (univ_inter _)

Composition of partial equivalence with full equivalence

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$ and a full equivalence $f'$ between $\beta$ and $\gamma$, the composition $e \circ f'$ is a partial equivalence between $\alpha$ and $\gamma$ where: - The source is $e.\text{source}$ (the domain where $e$ is defined) - The target is $f'^{-1}(e.\text{target})$ (the preimage of $e$'s target under $f'^{-1}$) - The forward function is $f' \circ e$ - The inverse function is $e^{-1} \circ f'^{-1}$ This composition maintains the partial equivalence property where the functions are mutual inverses when restricted to their respective domains.

PartialEquiv.transEquiv_eq_trans theorem

(e : PartialEquiv α β) (e' : β ≃ γ) : e.transEquiv e' = e.trans e'.toPartialEquiv

Full source

theorem transEquiv_eq_trans (e : PartialEquiv α β) (e' : β ≃ γ) :
    e.transEquiv e' = e.trans e'.toPartialEquiv :=
  copy_eq ..

Equality of Partial Equivalence Composition with Full Equivalence and its Partial Version

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$ and a full equivalence $e'$ between $\beta$ and $\gamma$, the composition of $e$ with $e'$ as a partial equivalence is equal to the composition of $e$ with the partial equivalence version of $e'$. In other words, $e \circ e' = e \circ (e' \text{ as partial equivalence})$.

PartialEquiv.transEquiv_transEquiv theorem

 (e : PartialEquiv α β) (f' : β ≃ γ) (f'' : γ ≃ δ) : (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')

Full source

@[simp, mfld_simps]
theorem transEquiv_transEquiv (e : PartialEquiv α β) (f' : β ≃ γ) (f'' : γ ≃ δ) :
    (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'') := by
  simp only [transEquiv_eq_trans, trans_assoc, Equiv.trans_toPartialEquiv]

Associativity of Partial Equivalence Composition with Full Equivalences

Informal description

Given a partial equivalence $e$ between types $\alpha$ and $\beta$, and full equivalences $f' : \beta \simeq \gamma$ and $f'' : \gamma \simeq \delta$, the following equality holds for compositions of partial equivalences: $$(e \circ f') \circ f'' = e \circ (f' \circ f'')$$ where $\circ$ denotes composition of partial equivalences with full equivalences.

PartialEquiv.trans_transEquiv theorem

 (e : PartialEquiv α β) (e' : PartialEquiv β γ) (f'' : γ ≃ δ) :
  (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')

Full source

@[simp, mfld_simps]
theorem trans_transEquiv (e : PartialEquiv α β) (e' : PartialEquiv β γ) (f'' : γ ≃ δ) :
    (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'') := by
  simp only [transEquiv_eq_trans, trans_assoc, Equiv.trans_toPartialEquiv]

Associativity of Partial Equivalence Composition with Full Equivalence

Informal description

For partial equivalences $e : \alpha \rightleftarrows \beta$ and $e' : \beta \rightleftarrows \gamma$, and a full equivalence $f'' : \gamma \simeq \delta$, the following equality holds: $$(e \circ e') \circ f'' = e \circ (e' \circ f'')$$ where $\circ$ denotes composition of partial equivalences (with the rightmost being a full equivalence converted to a partial equivalence).

Mathlib.Logic.Equiv.PartialEquiv

Main definitions

Implementation notes

Local coding conventions