Mathlib.Logic.Equiv.Set

EquivLike.range_eq_univ theorem

{α : Type*} {β : Type*} {E : Type*} [EquivLike E α β] (e : E) : range e = univ

Full source

@[simp]
theorem range_eq_univ {α : Type*} {β : Type*} {E : Type*} [EquivLike E α β] (e : E) :
    range e = univ :=
  eq_univ_of_forall (EquivLike.toEquiv e).surjective

Range of Equivalence-like Function is Universal Set

Informal description

For any type `E` that is an instance of `EquivLike` with parameters `α` and `β`, and for any element `e : E`, the range of `e` is equal to the universal set `univ` of `β`. In other words, the function represented by `e` is surjective.

Equiv.range_eq_univ theorem

{α : Type*} {β : Type*} (e : α ≃ β) : range e = univ

Full source

theorem range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) :
    range e = univ :=
  EquivLike.range_eq_univ e

Range of Equivalence is Universal Set

Informal description

For any equivalence $e \colon \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the range of $e$ is equal to the universal set of $\beta$, i.e., $\mathrm{range}(e) = \mathrm{univ}$.

Equiv.image_eq_preimage theorem

{α β} (e : α ≃ β) (s : Set α) : e '' s = e.symm ⁻¹' s

Full source

protected theorem image_eq_preimage {α β} (e : α ≃ β) (s : Set α) : e '' s = e.symm ⁻¹' s :=
  Set.ext fun _ => mem_image_iff_of_inverse e.left_inv e.right_inv

Image of a Set under an Equivalence Equals Preimage under its Inverse

Informal description

For any equivalence $e \colon \alpha \simeq \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $e$ is equal to the preimage of $s$ under the inverse equivalence $e^{-1}$, i.e., \[ e(s) = e^{-1}^{-1}(s). \]

Set.mem_image_equiv theorem

{α β} {S : Set α} {f : α ≃ β} {x : β} : x ∈ f '' S ↔ f.symm x ∈ S

Full source

@[simp 1001]
theorem _root_.Set.mem_image_equiv {α β} {S : Set α} {f : α ≃ β} {x : β} :
    x ∈ f '' Sx ∈ f '' S ↔ f.symm x ∈ S :=
  Set.ext_iff.mp (f.image_eq_preimage S) x

Characterization of Image Membership via Equivalence Inverse

Informal description

For any equivalence $f \colon \alpha \simeq \beta$, any subset $S \subseteq \alpha$, and any element $x \in \beta$, the element $x$ belongs to the image of $S$ under $f$ if and only if the inverse equivalence $f^{-1}$ maps $x$ back into $S$, i.e., \[ x \in f(S) \leftrightarrow f^{-1}(x) \in S. \]

Set.image_equiv_eq_preimage_symm theorem

{α β} (S : Set α) (f : α ≃ β) : f '' S = f.symm ⁻¹' S

Full source

/-- Alias for `Equiv.image_eq_preimage` -/
theorem _root_.Set.image_equiv_eq_preimage_symm {α β} (S : Set α) (f : α ≃ β) :
    f '' S = f.symm ⁻¹' S :=
  f.image_eq_preimage S

Image under Equivalence Equals Preimage under Inverse

Informal description

For any equivalence $f \colon \alpha \simeq \beta$ and any subset $S \subseteq \alpha$, the image of $S$ under $f$ is equal to the preimage of $S$ under the inverse equivalence $f^{-1}$, i.e., \[ f(S) = f^{-1}^{-1}(S). \]

Set.preimage_equiv_eq_image_symm theorem

{α β} (S : Set α) (f : β ≃ α) : f ⁻¹' S = f.symm '' S

Full source

/-- Alias for `Equiv.image_eq_preimage` -/
theorem _root_.Set.preimage_equiv_eq_image_symm {α β} (S : Set α) (f : β ≃ α) :
    f ⁻¹' S = f.symm '' S :=
  (f.symm.image_eq_preimage S).symm

Preimage under Equivalence Equals Image under Inverse

Informal description

For any equivalence $f \colon \beta \simeq \alpha$ and any subset $S \subseteq \alpha$, the preimage of $S$ under $f$ is equal to the image of $S$ under the inverse equivalence $f^{-1}$, i.e., \[ f^{-1}(S) = f^{-1}(S). \]

Equiv.symm_image_subset theorem

{α β} (e : α ≃ β) (s : Set α) (t : Set β) : e.symm '' t ⊆ s ↔ t ⊆ e '' s

Full source

@[simp high]
protected theorem symm_image_subset {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
    e.symm '' te.symm '' t ⊆ se.symm '' t ⊆ s ↔ t ⊆ e '' s := by rw [image_subset_iff, e.image_eq_preimage]

Image-Preimage Containment Relation for Equivalences

Informal description

For any equivalence $e \colon \alpha \simeq \beta$, any subset $s \subseteq \alpha$, and any subset $t \subseteq \beta$, the image of $t$ under $e^{-1}$ is contained in $s$ if and only if $t$ is contained in the image of $s$ under $e$. In symbols: \[ e^{-1}(t) \subseteq s \leftrightarrow t \subseteq e(s). \]

Equiv.subset_symm_image theorem

{α β} (e : α ≃ β) (s : Set α) (t : Set β) : s ⊆ e.symm '' t ↔ e '' s ⊆ t

Full source

@[simp high]
protected theorem subset_symm_image {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
    s ⊆ e.symm '' ts ⊆ e.symm '' t ↔ e '' s ⊆ t :=
  calc
    s ⊆ e.symm '' t ↔ e.symm.symm '' s ⊆ t := by rw [e.symm.symm_image_subset]
    _ ↔ e '' s ⊆ t := by rw [e.symm_symm]

Subset-Image Containment Relation for Equivalences

Informal description

For any equivalence $e \colon \alpha \simeq \beta$, any subset $s \subseteq \alpha$, and any subset $t \subseteq \beta$, the subset $s$ is contained in the image of $t$ under $e^{-1}$ if and only if the image of $s$ under $e$ is contained in $t$. In symbols: \[ s \subseteq e^{-1}(t) \leftrightarrow e(s) \subseteq t. \]

Equiv.symm_image_image theorem

{α β} (e : α ≃ β) (s : Set α) : e.symm '' (e '' s) = s

Full source

@[simp]
theorem symm_image_image {α β} (e : α ≃ β) (s : Set α) : e.symm '' (e '' s) = s :=
  e.leftInverse_symm.image_image s

Preimage of Image under Equivalence is Original Set

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any subset $s \subseteq \alpha$, the preimage under $e^{-1}$ of the image of $s$ under $e$ equals $s$, i.e., $e^{-1}(e(s)) = s$.

Equiv.image_symm_image theorem

{α β} (e : α ≃ β) (s : Set β) : e '' (e.symm '' s) = s

Full source

@[simp]
theorem image_symm_image {α β} (e : α ≃ β) (s : Set β) : e '' (e.symm '' s) = s :=
  e.symm.symm_image_image s

Image of Symmetric Preimage under Equivalence is Identity

Informal description

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

Equiv.image_preimage theorem

{α β} (e : α ≃ β) (s : Set β) : e '' (e ⁻¹' s) = s

Full source

@[simp]
theorem image_preimage {α β} (e : α ≃ β) (s : Set β) : e '' (e ⁻¹' s) = s :=
  e.surjective.image_preimage s

Image of Preimage under Equivalence is Identity

Informal description

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

Equiv.preimage_image theorem

{α β} (e : α ≃ β) (s : Set α) : e ⁻¹' (e '' s) = s

Full source

@[simp]
theorem preimage_image {α β} (e : α ≃ β) (s : Set α) : e ⁻¹' (e '' s) = s :=
  e.injective.preimage_image s

Preimage of Image under Equivalence is Identity

Informal description

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

Equiv.image_compl theorem

{α β} (f : Equiv α β) (s : Set α) : f '' sᶜ = (f '' s)ᶜ

Full source

protected theorem image_compl {α β} (f : Equiv α β) (s : Set α) : f '' sᶜ = (f '' s)ᶜ :=
  image_compl_eq f.bijective

Image of Complement under Equivalence Equals Complement of Image

Informal description

For any equivalence $f : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the image of the complement of $s$ under $f$ equals the complement of the image of $s$ under $f$. In symbols, $f(s^c) = (f(s))^c$.

Equiv.symm_preimage_preimage theorem

{α β} (e : α ≃ β) (s : Set β) : e.symm ⁻¹' (e ⁻¹' s) = s

Full source

@[simp]
theorem symm_preimage_preimage {α β} (e : α ≃ β) (s : Set β) : e.symm ⁻¹' (e ⁻¹' s) = s :=
  e.rightInverse_symm.preimage_preimage s

Double Preimage Identity for Equivalences

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subset $s \subseteq \beta$, the preimage of $s$ under $e$ followed by the preimage under $e^{-1}$ equals $s$. That is, $e^{-1}(e^{-1}(s)) = s$.

Equiv.preimage_symm_preimage theorem

{α β} (e : α ≃ β) (s : Set α) : e ⁻¹' (e.symm ⁻¹' s) = s

Full source

@[simp]
theorem preimage_symm_preimage {α β} (e : α ≃ β) (s : Set α) : e ⁻¹' (e.symm ⁻¹' s) = s :=
  e.leftInverse_symm.preimage_preimage s

Double Symmetric Preimage Identity for Equivalences

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the preimage of $s$ under $e^{-1}$ followed by the preimage under $e$ equals $s$. That is, $e^{-1}(e^{-1}(s)) = s$.

Equiv.preimage_subset theorem

{α β} (e : α ≃ β) (s t : Set β) : e ⁻¹' s ⊆ e ⁻¹' t ↔ s ⊆ t

Full source

theorem preimage_subset {α β} (e : α ≃ β) (s t : Set β) : e ⁻¹' se ⁻¹' s ⊆ e ⁻¹' te ⁻¹' s ⊆ e ⁻¹' t ↔ s ⊆ t :=
  e.surjective.preimage_subset_preimage_iff

Preimage Subset Preservation under Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subsets $s, t \subseteq \beta$, the preimage of $s$ under $e$ is a subset of the preimage of $t$ under $e$ if and only if $s$ is a subset of $t$. That is, $e^{-1}(s) \subseteq e^{-1}(t) \leftrightarrow s \subseteq t$.

Equiv.image_subset theorem

{α β} (e : α ≃ β) (s t : Set α) : e '' s ⊆ e '' t ↔ s ⊆ t

Full source

theorem image_subset {α β} (e : α ≃ β) (s t : Set α) : e '' se '' s ⊆ e '' te '' s ⊆ e '' t ↔ s ⊆ t :=
  image_subset_image_iff e.injective

Image Subset Preservation under Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subsets $s, t \subseteq \alpha$, the image of $s$ under $e$ is contained in the image of $t$ under $e$ if and only if $s$ is contained in $t$. That is, $e(s) \subseteq e(t) \leftrightarrow s \subseteq t$.

Equiv.image_eq_iff_eq theorem

{α β} (e : α ≃ β) (s t : Set α) : e '' s = e '' t ↔ s = t

Full source

@[simp]
theorem image_eq_iff_eq {α β} (e : α ≃ β) (s t : Set α) : e '' se '' s = e '' t ↔ s = t :=
  image_eq_image e.injective

Image Equality under Equivalence iff Set Equality

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subsets $s, t \subseteq \alpha$, the image of $s$ under $e$ is equal to the image of $t$ under $e$ if and only if $s$ is equal to $t$. That is, $e(s) = e(t) \leftrightarrow s = t$.

Equiv.preimage_eq_iff_eq_image theorem

{α β} (e : α ≃ β) (s t) : e ⁻¹' s = t ↔ s = e '' t

Full source

theorem preimage_eq_iff_eq_image {α β} (e : α ≃ β) (s t) : e ⁻¹' se ⁻¹' s = t ↔ s = e '' t :=
  Set.preimage_eq_iff_eq_image e.bijective

Preimage-Image Correspondence under Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and any subsets $s \subseteq \beta$ and $t \subseteq \alpha$, the preimage of $s$ under $e$ is equal to $t$ if and only if $s$ is equal to the image of $t$ under $e$. That is, $e^{-1}(s) = t \leftrightarrow s = e(t)$.

Equiv.setOf_apply_symm_eq_image_setOf theorem

{α β} (e : α ≃ β) (p : α → Prop) : {b | p (e.symm b)} = e '' {a | p a}

Full source

lemma setOf_apply_symm_eq_image_setOf {α β} (e : α ≃ β) (p : α → Prop) :
    {b | p (e.symm b)} = e '' {a | p a} := by
  rw [Equiv.image_eq_preimage, preimage_setOf_eq]

Equivalence of Preimage Set and Image Set under Predicate

Informal description

For any equivalence $e \colon \alpha \simeq \beta$ and any predicate $p \colon \alpha \to \mathrm{Prop}$, the set of elements $b \in \beta$ satisfying $p(e^{-1}(b))$ is equal to the image under $e$ of the set of elements $a \in \alpha$ satisfying $p(a)$. In symbols: \[ \{b \in \beta \mid p(e^{-1}(b))\} = e(\{a \in \alpha \mid p(a)\}). \]

Equiv.prod_assoc_preimage theorem

{α β γ} {s : Set α} {t : Set β} {u : Set γ} : Equiv.prodAssoc α β γ ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Full source

@[simp]
theorem prod_assoc_preimage {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    Equiv.prodAssocEquiv.prodAssoc α β γ ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u := by
  ext
  simp [and_assoc]

Preimage of Product under Associativity Equivalence

Informal description

For any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, the preimage of $s \times t \times u$ under the associativity equivalence $\text{prodAssoc}_{\alpha,\beta,\gamma}$ is equal to $(s \times t) \times u$.

Equiv.prod_assoc_symm_preimage theorem

 {α β γ} {s : Set α} {t : Set β} {u : Set γ} : (Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Full source

@[simp]
theorem prod_assoc_symm_preimage {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    (Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u := by
  ext
  simp [and_assoc]

Preimage of Product under Associativity Equivalence Inverse

Informal description

For any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, the preimage of $(s \times t) \times u$ under the inverse of the associativity equivalence $\text{prodAssoc}_{\alpha,\beta,\gamma}$ is equal to $s \times (t \times u)$.

Equiv.prod_assoc_image theorem

{α β γ} {s : Set α} {t : Set β} {u : Set γ} : Equiv.prodAssoc α β γ '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Full source

theorem prod_assoc_image {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    Equiv.prodAssocEquiv.prodAssoc α β γ '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u := by
  simpa only [Equiv.image_eq_preimage] using prod_assoc_symm_preimage

Image of Product under Associativity Equivalence Equals Reassociated Product

Informal description

For any types $\alpha$, $\beta$, $\gamma$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, $u \subseteq \gamma$, the image of the product set $(s \times t) \times u$ under the associativity equivalence $\text{prodAssoc}_{\alpha,\beta,\gamma} \colon (\alpha \times \beta) \times \gamma \simeq \alpha \times (\beta \times \gamma)$ equals the product set $s \times (t \times u)$.

Equiv.prod_assoc_symm_image theorem

 {α β γ} {s : Set α} {t : Set β} {u : Set γ} : (Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Full source

theorem prod_assoc_symm_image {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    (Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u := by
  simpa only [Equiv.image_eq_preimage] using prod_assoc_preimage

Image of Product under Inverse Associativity Equivalence Equals Reassociated Product

Informal description

For any types $\alpha$, $\beta$, $\gamma$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, $u \subseteq \gamma$, the image of the product set $s \times (t \times u)$ under the inverse of the associativity equivalence $\text{prodAssoc}_{\alpha,\beta,\gamma} \colon \alpha \times (\beta \times \gamma) \simeq (\alpha \times \beta) \times \gamma$ equals the product set $(s \times t) \times u$.

Equiv.setProdEquivSigma definition

{α β : Type*} (s : Set (α × β)) : s ≃ Σ x : α, {y : β | (x, y) ∈ s}

Full source

/-- A set `s` in `α × β` is equivalent to the sigma-type `Σ x, {y | (x, y) ∈ s}`. -/
def setProdEquivSigma {α β : Type*} (s : Set (α × β)) :
    s ≃ Σx : α, { y : β | (x, y) ∈ s } where
  toFun x := ⟨x.1.1, x.1.2, by simp⟩
  invFun x := ⟨(x.1, x.2.1), x.2.2⟩
  left_inv := fun ⟨⟨_, _⟩, _⟩ => rfl
  right_inv := fun ⟨_, _, _⟩ => rfl

Equivalence between a subset of a product and its sigma-type representation

Informal description

For any types $\alpha$ and $\beta$, and any subset $s$ of the Cartesian product $\alpha \times \beta$, there is an equivalence between $s$ and the sigma-type $\Sigma x : \alpha, \{y \in \beta \mid (x, y) \in s\}$. The equivalence maps each element $(x, y) \in s$ to the pair $(x, y)$ in the sigma-type (with proof that $(x, y) \in s$), and conversely maps each $(x, y, h)$ in the sigma-type back to $((x, y), h)$ in $s$.

Equiv.setCongr definition

{α : Type*} {s t : Set α} (h : s = t) : s ≃ t

Full source

/-- The subtypes corresponding to equal sets are equivalent. -/
@[simps! apply symm_apply]
def setCongr {α : Type*} {s t : Set α} (h : s = t) : s ≃ t :=
  subtypeEquivProp h

Equivalence of equal sets

Informal description

Given a type $\alpha$ and two subsets $s, t \subseteq \alpha$ that are equal ($s = t$), the subtypes corresponding to $s$ and $t$ are equivalent as types.

Equiv.image definition

{α β : Type*} (e : α ≃ β) (s : Set α) : s ≃ e '' s

Full source

/-- A set is equivalent to its image under an equivalence.
-/
@[simps]
def image {α β : Type*} (e : α ≃ β) (s : Set α) :
    s ≃ e '' s where
  toFun x := ⟨e x.1, by simp⟩
  invFun y :=
    ⟨e.symm y.1, by
      rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩
      simpa using m⟩
  left_inv x := by simp
  right_inv y := by simp

Equivalence between a set and its image under an equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and a subset $s \subseteq \alpha$, the set $s$ is equivalent to its image $e(s) \subseteq \beta$ under the equivalence $e$. The equivalence maps each element $x \in s$ to $e(x) \in e(s)$, and its inverse maps each $y \in e(s)$ back to $e^{-1}(y) \in s$.

Equiv.Set.univ definition

(α) : @univ α ≃ α

Full source

/-- `univ α` is equivalent to `α`. -/
@[simps apply symm_apply]
protected def univ (α) : @univ α ≃ α :=
  ⟨Subtype.val, fun a => ⟨a, trivial⟩, fun ⟨_, _⟩ => rfl, fun _ => rfl⟩

Equivalence between universal set and base type

Informal description

The universal set of a type $\alpha$ is equivalent to $\alpha$ itself. Specifically, there exists a bijection between the set of all elements of type $\alpha$ (denoted as `univ α`) and $\alpha$, where the bijection is given by the inclusion map and its inverse maps each element to itself in the universal set.

Equiv.Set.empty definition

(α) : (∅ : Set α) ≃ Empty

Full source

/-- An empty set is equivalent to the `Empty` type. -/
protected def empty (α) : (∅ : Set α) ≃ Empty :=
  equivEmpty _

Equivalence between empty set and empty type

Informal description

The empty set in a type $\alpha$ is equivalent to the empty type `Empty`. This means there exists a bijection between the empty set and the empty type.

Equiv.Set.pempty definition

(α) : (∅ : Set α) ≃ PEmpty

Full source

/-- An empty set is equivalent to a `PEmpty` type. -/
protected def pempty (α) : (∅ : Set α) ≃ PEmpty :=
  equivPEmpty _

Empty set equivalence to `PEmpty`

Informal description

The empty set $\emptyset$ in a type $\alpha$ is equivalent to the type `PEmpty`, which is the empty type in Lean's universe of propositions.

Equiv.Set.union' definition

 {α} {s t : Set α} (p : α → Prop) [DecidablePred p] (hs : ∀ x ∈ s, p x) (ht : ∀ x ∈ t, ¬p x) : (s ∪ t : Set α) ≃ s ⊕ t

Full source

/-- If sets `s` and `t` are separated by a decidable predicate, then `s ∪ t` is equivalent to
`s ⊕ t`. -/
protected def union' {α} {s t : Set α} (p : α → Prop) [DecidablePred p] (hs : ∀ x ∈ s, p x)
    (ht : ∀ x ∈ t, ¬p x) : (s ∪ t : Set α) ≃ s ⊕ t where
  toFun x :=
    if hp : p x then Sum.inl ⟨_, x.2.resolve_right fun xt => ht _ xt hp⟩
    else Sum.inr ⟨_, x.2.resolve_left fun xs => hp (hs _ xs)⟩
  invFun o :=
    match o with
    | Sum.inl x => ⟨x, Or.inl x.2⟩
    | Sum.inr x => ⟨x, Or.inr x.2⟩
  left_inv := fun ⟨x, h'⟩ => by by_cases h : p x <;> simp [h]
  right_inv o := by
    rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]

Equivalence between union and sum of separated sets

Informal description

Given two sets $s$ and $t$ in a type $\alpha$ and a decidable predicate $p$ on $\alpha$, if every element of $s$ satisfies $p$ and no element of $t$ satisfies $p$, then the union $s \cup t$ is equivalent to the disjoint union $s \oplus t$.

Equiv.Set.union definition

{α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) : (s ∪ t : Set α) ≃ s ⊕ t

Full source

/-- If sets `s` and `t` are disjoint, then `s ∪ t` is equivalent to `s ⊕ t`. -/
protected def union {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) :
    (s ∪ t : Set α) ≃ s ⊕ t :=
  Set.union' (fun x => x ∈ s) (fun _ => id) fun _ xt xs => Set.disjoint_left.mp H xs xt

Equivalence between union of disjoint sets and their sum

Informal description

Given two disjoint sets $s$ and $t$ in a type $\alpha$, with a decidable predicate for membership in $s$, the union $s \cup t$ is equivalent to the disjoint union $s \oplus t$.

Equiv.Set.union_apply_left theorem

 {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : (s ∪ t : Set α)} (ha : ↑a ∈ s) :
  Equiv.Set.union H a = Sum.inl ⟨a, ha⟩

Full source

theorem union_apply_left {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t)
    {a : (s ∪ t : Set α)} (ha : ↑a ∈ s) : Equiv.Set.union H a = Sum.inl ⟨a, ha⟩ :=
  dif_pos ha

Mapping of Union Element to Left Summand in Disjoint Union Equivalence

Informal description

Given two disjoint sets $s$ and $t$ in a type $\alpha$, with a decidable predicate for membership in $s$, and an element $a$ in their union $s \cup t$ such that $a \in s$, the equivalence `Equiv.Set.union` maps $a$ to the left inclusion $\text{Sum.inl} \langle a, ha \rangle$ in the disjoint union $s \oplus t$.

Equiv.Set.union_apply_right theorem

 {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : (s ∪ t : Set α)} (ha : ↑a ∈ t) :
  Equiv.Set.union H a = Sum.inr ⟨a, ha⟩

Full source

theorem union_apply_right {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t)
    {a : (s ∪ t : Set α)} (ha : ↑a ∈ t) : Equiv.Set.union H a = Sum.inr ⟨a, ha⟩ :=
  dif_neg fun h => Set.disjoint_left.mp H h ha

Mapping of Union Element to Right Summand in Disjoint Union Equivalence

Informal description

Given two disjoint sets $s$ and $t$ in a type $\alpha$, with a decidable predicate for membership in $s$, and an element $a$ in their union $s \cup t$ such that $a \in t$, the equivalence `Equiv.Set.union` maps $a$ to the right inclusion $\text{Sum.inr} \langle a, ha \rangle$ in the disjoint union $s \oplus t$.

Equiv.Set.union_symm_apply_left theorem

 {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) (a : s) :
  (Equiv.Set.union H).symm (Sum.inl a) = ⟨a, by simp⟩

Full source

@[simp]
theorem union_symm_apply_left {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t)
    (a : s) : (Equiv.Set.union H).symm (Sum.inl a) = ⟨a, by simp⟩ :=
  rfl

Inverse of Union Equivalence Applied to Left Inclusion

Informal description

Let $\alpha$ be a type, and let $s, t \subseteq \alpha$ be disjoint sets with a decidable membership predicate for $s$. For any element $a \in s$, the inverse of the equivalence $\text{Equiv.Set.union}\ H$ applied to the left inclusion $\text{Sum.inl}\ a$ equals the element $\langle a, \text{by simp} \rangle$ in the union $s \cup t$.

Equiv.Set.union_symm_apply_right theorem

 {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) (a : t) :
  (Equiv.Set.union H).symm (Sum.inr a) = ⟨a, by simp⟩

Full source

@[simp]
theorem union_symm_apply_right {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t)
    (a : t) : (Equiv.Set.union H).symm (Sum.inr a) = ⟨a, by simp⟩ :=
  rfl

Inverse of Union Equivalence Applied to Right Inclusion

Informal description

Let $\alpha$ be a type, and let $s, t \subseteq \alpha$ be disjoint sets with a decidable membership predicate for $s$. For any element $a \in t$, the inverse of the equivalence $\text{Equiv.Set.union}\ H$ applied to the right inclusion $\text{Sum.inr}\ a$ equals the element $\langle a, \text{by simp} \rangle$ in the union $s \cup t$.

Equiv.Set.singleton definition

{α} (a : α) : ({ a } : Set α) ≃ PUnit.{u}

Full source

/-- A singleton set is equivalent to a `PUnit` type. -/
protected def singleton {α} (a : α) : ({a} : Set α) ≃ PUnit.{u} :=
  ⟨fun _ => PUnit.unit, fun _ => ⟨a, mem_singleton _⟩, fun ⟨x, h⟩ => by
    simp? at h says simp only [mem_singleton_iff] at h
    subst x
    rfl, fun ⟨⟩ => rfl⟩

Equivalence between a singleton set and the unit type

Informal description

For any type $\alpha$ and element $a \in \alpha$, the singleton set $\{a\}$ is equivalent to the unit type $\text{PUnit}$.

Equiv.Set.Equiv.strictMono_setCongr theorem

{α : Type*} [Preorder α] {S T : Set α} (h : S = T) : StrictMono (setCongr h)

Full source

lemma Equiv.strictMono_setCongr {α : Type*} [Preorder α] {S T : Set α} (h : S = T) :
    StrictMono (setCongr h) := fun _ _ ↦ id

Strict Monotonicity of the Set Equivalence Induced by Equality

Informal description

Let $\alpha$ be a type equipped with a preorder, and let $S, T \subseteq \alpha$ be subsets such that $S = T$. Then the equivalence $\text{setCongr}\ h$ (induced by the equality $h : S = T$) is strictly monotone.

Equiv.Set.insert definition

{α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) : (insert a s : Set α) ≃ s ⊕ PUnit.{u + 1}

Full source

/-- If `a ∉ s`, then `insert a s` is equivalent to `s ⊕ PUnit`. -/
protected def insert {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) :
    (insert a s : Set α) ≃ s ⊕ PUnit.{u + 1} :=
  calc
    (insert a s : Set α) ≃ ↥(s ∪ {a}) := Equiv.setCongr (by simp)
    _ ≃ s ⊕ ({a} : Set α)calc
    (insert a s : Set α) ≃ ↥(s ∪ {a}) := Equiv.setCongr (by simp)
    _ ≃ s ⊕ ({a} : Set α) := Equiv.Set.union <| by simpa
    _ ≃ s ⊕ PUnit.{u + 1} := sumCongr (Equiv.refl _) (Equiv.Set.singleton _)

Equivalence between insertion into a set and disjoint union with unit type

Informal description

Given a type $\alpha$, a subset $s \subseteq \alpha$ with a decidable membership predicate, and an element $a \in \alpha$ such that $a \notin s$, the set $\{a\} \cup s$ is equivalent to the disjoint union of $s$ with the unit type $\text{PUnit}$.

Equiv.Set.insert_symm_apply_inl theorem

 {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) (b : s) :
  (Equiv.Set.insert H).symm (Sum.inl b) = ⟨b, Or.inr b.2⟩

Full source

@[simp]
theorem insert_symm_apply_inl {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s)
    (b : s) : (Equiv.Set.insert H).symm (Sum.inl b) = ⟨b, Or.inr b.2⟩ :=
  rfl

Inverse Mapping of Left Summand in Set Insertion Equivalence

Informal description

Given a type $\alpha$, a subset $s \subseteq \alpha$ with a decidable membership predicate, and an element $a \in \alpha$ such that $a \notin s$, the inverse of the equivalence $\text{Equiv.Set.insert}\ H$ maps the left summand $\text{Sum.inl}\ b$ (where $b$ is an element of $s$) to the element $\langle b, \text{Or.inr}\ b.2 \rangle$ in the set $\{a\} \cup s$.

Equiv.Set.insert_symm_apply_inr theorem

 {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) (b : PUnit.{u + 1}) :
  (Equiv.Set.insert H).symm (Sum.inr b) = ⟨a, Or.inl rfl⟩

Full source

@[simp]
theorem insert_symm_apply_inr {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s)
    (b : PUnitPUnit.{u + 1}) : (Equiv.Set.insert H).symm (Sum.inr b) = ⟨a, Or.inl rfl⟩ :=
  rfl

Inverse Mapping of Unit Element to Inserted Element in Set Equivalence

Informal description

Given a type $\alpha$, a subset $s \subseteq \alpha$ with a decidable membership predicate, and an element $a \in \alpha$ such that $a \notin s$, the inverse of the equivalence `Equiv.Set.insert H` maps the right summand $\text{Sum.inr b}$ (where $b$ is an element of the unit type $\text{PUnit}$) to the element $\langle a, \text{Or.inl rfl}\rangle$ in the set $\{a\} \cup s$.

Equiv.Set.insert_apply_left theorem

 {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) :
  Equiv.Set.insert H ⟨a, Or.inl rfl⟩ = Sum.inr PUnit.unit

Full source

@[simp]
theorem insert_apply_left {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) :
    Equiv.Set.insert H ⟨a, Or.inl rfl⟩ = Sum.inr PUnit.unit :=
  (Equiv.Set.insert H).apply_eq_iff_eq_symm_apply.2 rfl

Mapping of Inserted Element to Unit Type in Set Equivalence

Informal description

Given a type $\alpha$, a subset $s \subseteq \alpha$ with a decidable membership predicate, and an element $a \in \alpha$ such that $a \notin s$, the equivalence `Equiv.Set.insert H` maps the element $\langle a, \text{Or.inl rfl}\rangle$ (which represents $a$ in the inserted set $\{a\} \cup s$) to the right summand $\text{Sum.inr PUnit.unit}$ of the disjoint union $s \oplus \text{PUnit}$.

Equiv.Set.insert_apply_right theorem

 {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) (b : s) :
  Equiv.Set.insert H ⟨b, Or.inr b.2⟩ = Sum.inl b

Full source

@[simp]
theorem insert_apply_right {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) (b : s) :
    Equiv.Set.insert H ⟨b, Or.inr b.2⟩ = Sum.inl b :=
  (Equiv.Set.insert H).apply_eq_iff_eq_symm_apply.2 rfl

Mapping of Existing Element to Original Set in Insertion Equivalence

Informal description

Given a type $\alpha$, a subset $s \subseteq \alpha$ with a decidable membership predicate, and an element $a \in \alpha$ such that $a \notin s$, the equivalence `Equiv.Set.insert H` maps an element $\langle b, \text{Or.inr b.2}\rangle$ (where $b \in s$) to the left summand $\text{Sum.inl b}$ of the disjoint union $s \oplus \text{PUnit}$.

Equiv.Set.sumCompl definition

{α} (s : Set α) [DecidablePred (· ∈ s)] : s ⊕ (sᶜ : Set α) ≃ α

Full source

/-- If `s : Set α` is a set with decidable membership, then `s ⊕ sᶜ` is equivalent to `α`. -/
protected def sumCompl {α} (s : Set α) [DecidablePred (· ∈ s)] : s ⊕ (sᶜ : Set α)s ⊕ (sᶜ : Set α) ≃ α :=
  calc
    s ⊕ (sᶜ : Set α) ≃ ↥(s ∪ sᶜ) := (Equiv.Set.union disjoint_compl_right).symm
    _ ≃ @univ αcalc
    s ⊕ (sᶜ : Set α) ≃ ↥(s ∪ sᶜ) := (Equiv.Set.union disjoint_compl_right).symm
    _ ≃ @univ α := Equiv.setCongr (by simp)
    _ ≃ α := Equiv.Set.univ _

Equivalence between a set and its complement via disjoint union

Informal description

Given a type $\alpha$ and a subset $s \subseteq \alpha$ with decidable membership, the disjoint union of $s$ and its complement $s^c$ is equivalent to $\alpha$ itself. This equivalence is constructed by first showing that $s \cup s^c$ is equivalent to the universal set of $\alpha$, which in turn is equivalent to $\alpha$.

Equiv.Set.sumCompl_apply_inl theorem

{α : Type u} (s : Set α) [DecidablePred (· ∈ s)] (x : s) : Equiv.Set.sumCompl s (Sum.inl x) = x

Full source

@[simp]
theorem sumCompl_apply_inl {α : Type u} (s : Set α) [DecidablePred (· ∈ s)] (x : s) :
    Equiv.Set.sumCompl s (Sum.inl x) = x :=
  rfl

Left Inclusion in Sum-Complement Equivalence Maps to Original Element

Informal description

For any type $\alpha$, a subset $s \subseteq \alpha$ with decidable membership, and an element $x \in s$, the equivalence `Equiv.Set.sumCompl` maps the left inclusion $\text{Sum.inl}(x)$ to $x$ itself.

Equiv.Set.sumCompl_apply_inr theorem

{α : Type u} (s : Set α) [DecidablePred (· ∈ s)] (x : (sᶜ : Set α)) : Equiv.Set.sumCompl s (Sum.inr x) = x

Full source

@[simp]
theorem sumCompl_apply_inr {α : Type u} (s : Set α) [DecidablePred (· ∈ s)] (x : (sᶜ : Set α)) :
    Equiv.Set.sumCompl s (Sum.inr x) = x :=
  rfl

Right Inclusion in Sum-Complement Equivalence Maps to Original Element

Informal description

For any type $\alpha$, a subset $s \subseteq \alpha$ with decidable membership, and an element $x$ in the complement $s^c$, the equivalence `Equiv.Set.sumCompl` maps the right inclusion $\text{Sum.inr}(x)$ to $x$ itself.

Equiv.Set.sumCompl_symm_apply_of_mem theorem

 {α : Type u} {s : Set α} [DecidablePred (· ∈ s)] {x : α} (hx : x ∈ s) : (Equiv.Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩

Full source

theorem sumCompl_symm_apply_of_mem {α : Type u} {s : Set α} [DecidablePred (· ∈ s)] {x : α}
    (hx : x ∈ s) : (Equiv.Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩ := by
  simp [Equiv.Set.sumCompl, Equiv.Set.univ, union_apply_left, hx]

Inverse of Sum-Complement Equivalence Maps Element to Left Summand When in Set

Informal description

For any type $\alpha$, a subset $s \subseteq \alpha$ with decidable membership, and an element $x \in \alpha$ that belongs to $s$, the inverse of the equivalence `Equiv.Set.sumCompl` maps $x$ to the left inclusion $\text{Sum.inl} \langle x, hx \rangle$ in the disjoint union $s \oplus s^c$, where $hx$ is the proof that $x \in s$.

Equiv.Set.sumCompl_symm_apply_of_not_mem theorem

 {α : Type u} {s : Set α} [DecidablePred (· ∈ s)] {x : α} (hx : x ∉ s) : (Equiv.Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩

Full source

theorem sumCompl_symm_apply_of_not_mem {α : Type u} {s : Set α} [DecidablePred (· ∈ s)] {x : α}
    (hx : x ∉ s) : (Equiv.Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩ := by
  simp [Equiv.Set.sumCompl, Equiv.Set.univ, union_apply_right, hx]

Inverse of Sum-Complement Equivalence Maps Non-Member to Right Summand

Informal description

For any type $\alpha$, a subset $s \subseteq \alpha$ with decidable membership, and an element $x \in \alpha$ that does not belong to $s$, the inverse of the equivalence `Equiv.Set.sumCompl` maps $x$ to the right inclusion $\text{Sum.inr} \langle x, hx \rangle$ in the disjoint union $s \oplus s^c$, where $hx$ is the proof that $x \notin s$.

Equiv.Set.sumCompl_symm_apply theorem

{α : Type*} {s : Set α} [DecidablePred (· ∈ s)] {x : s} : (Equiv.Set.sumCompl s).symm x = Sum.inl x

Full source

@[simp]
theorem sumCompl_symm_apply {α : Type*} {s : Set α} [DecidablePred (· ∈ s)] {x : s} :
    (Equiv.Set.sumCompl s).symm x = Sum.inl x :=
  Set.sumCompl_symm_apply_of_mem x.2

Inverse of Sum-Complement Equivalence Maps Set Element to Left Summand

Informal description

For any type $\alpha$ and a subset $s \subseteq \alpha$ with decidable membership, the inverse of the equivalence $\text{sumCompl}$ maps an element $x \in s$ to the left inclusion $\text{Sum.inl}(x)$ in the disjoint union $s \oplus s^c$.

Equiv.Set.sumCompl_symm_apply_compl theorem

{α : Type*} {s : Set α} [DecidablePred (· ∈ s)] {x : (sᶜ : Set α)} : (Equiv.Set.sumCompl s).symm x = Sum.inr x

Full source

@[simp]
theorem sumCompl_symm_apply_compl {α : Type*} {s : Set α} [DecidablePred (· ∈ s)]
    {x : (sᶜ : Set α)} : (Equiv.Set.sumCompl s).symm x = Sum.inr x :=
  Set.sumCompl_symm_apply_of_not_mem x.2

Inverse of Sum-Complement Equivalence Maps Complement Elements to Right Summand

Informal description

For any type $\alpha$ and a subset $s \subseteq \alpha$ with decidable membership, the inverse of the equivalence $\text{sumCompl}$ maps an element $x$ in the complement $s^c$ to the right inclusion $\text{Sum.inr}(x)$ in the disjoint union $s \oplus s^c$.

Equiv.Set.sumDiffSubset definition

{α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] : s ⊕ (t \ s : Set α) ≃ t

Full source

/-- `sumDiffSubset s t` is the natural equivalence between
`s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets. -/
protected def sumDiffSubset {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] :
    s ⊕ (t \ s : Set α)s ⊕ (t \ s : Set α) ≃ t :=
  calc
    s ⊕ (t \ s : Set α) ≃ (s ∪ t \ s : Set α) :=
      (Equiv.Set.union disjoint_sdiff_self_right).symm
    _ ≃ t := Equiv.setCongr (by simp [union_diff_self, union_eq_self_of_subset_left h])

Equivalence between sum of subset and its complement in a larger set

Informal description

Given a type $\alpha$ and two subsets $s, t \subseteq \alpha$ with $s \subseteq t$, the natural equivalence between the disjoint union $s \oplus (t \setminus s)$ and $t$ is constructed by first showing that $s \oplus (t \setminus s)$ is equivalent to $s \cup (t \setminus s)$ (using the disjointness of $s$ and $t \setminus s$), and then observing that $s \cup (t \setminus s) = t$ when $s \subseteq t$.

Equiv.Set.sumDiffSubset_apply_inl theorem

 {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] (x : s) : Equiv.Set.sumDiffSubset h (Sum.inl x) = inclusion h x

Full source

@[simp]
theorem sumDiffSubset_apply_inl {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] (x : s) :
    Equiv.Set.sumDiffSubset h (Sum.inl x) = inclusion h x :=
  rfl

Application of Sum-Diff-Subset Equivalence to Left Summand

Informal description

For any type $\alpha$ and subsets $s, t \subseteq \alpha$ with $s \subseteq t$, the equivalence $\text{sumDiffSubset}$ maps the left summand $\text{Sum.inl}(x)$ (where $x \in s$) to the inclusion of $x$ in $t$ via the natural embedding $h : s \hookrightarrow t$.

Equiv.Set.sumDiffSubset_apply_inr theorem

 {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] (x : (t \ s : Set α)) :
  Equiv.Set.sumDiffSubset h (Sum.inr x) = inclusion diff_subset x

Full source

@[simp]
theorem sumDiffSubset_apply_inr {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)]
    (x : (t \ s : Set α)) : Equiv.Set.sumDiffSubset h (Sum.inr x) = inclusion diff_subset x :=
  rfl

Application of Sum-Diff-Subset Equivalence to Right Summand

Informal description

For any type $\alpha$ and subsets $s, t \subseteq \alpha$ with $s \subseteq t$, if $x$ is an element of the set difference $t \setminus s$, then the equivalence $\text{sumDiffSubset}$ maps the right summand $\text{Sum.inr}(x)$ to the inclusion of $x$ in $t$ via the natural embedding $\text{diff\_subset} : t \setminus s \hookrightarrow t$.

Equiv.Set.sumDiffSubset_symm_apply_of_mem theorem

 {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] {x : t} (hx : x.1 ∈ s) :
  (Equiv.Set.sumDiffSubset h).symm x = Sum.inl ⟨x, hx⟩

Full source

theorem sumDiffSubset_symm_apply_of_mem {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)]
    {x : t} (hx : x.1 ∈ s) : (Equiv.Set.sumDiffSubset h).symm x = Sum.inl ⟨x, hx⟩ := by
  apply (Equiv.Set.sumDiffSubset h).injective
  simp only [apply_symm_apply, sumDiffSubset_apply_inl, Set.inclusion_mk]

Inverse of Sum-Diff-Subset Equivalence for Membership Case

Informal description

Given a type $\alpha$ and subsets $s, t \subseteq \alpha$ with $s \subseteq t$, if $x \in t$ and $x \in s$, then the inverse of the equivalence $\text{sumDiffSubset}$ maps $x$ to the left summand $\text{inl}$ of the pair $\langle x, x \in s \rangle$.

Equiv.Set.sumDiffSubset_symm_apply_of_not_mem theorem

 {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] {x : t} (hx : x.1 ∉ s) :
  (Equiv.Set.sumDiffSubset h).symm x = Sum.inr ⟨x, ⟨x.2, hx⟩⟩

Full source

theorem sumDiffSubset_symm_apply_of_not_mem {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)]
    {x : t} (hx : x.1 ∉ s) : (Equiv.Set.sumDiffSubset h).symm x = Sum.inr ⟨x, ⟨x.2, hx⟩⟩ := by
  apply (Equiv.Set.sumDiffSubset h).injective
  simp only [apply_symm_apply, sumDiffSubset_apply_inr, Set.inclusion_mk]

Inverse of Sum-Diff-Subset Equivalence for Non-Membership Case

Informal description

Given a type $\alpha$ and subsets $s, t \subseteq \alpha$ with $s \subseteq t$, if $x \in t$ and $x \notin s$, then the inverse of the equivalence $\text{sumDiffSubset}$ maps $x$ to the right summand $\text{inr}$ of the pair $\langle x, \langle x \in t, x \notin s \rangle \rangle$.

Equiv.Set.unionSumInter definition

{α : Type u} (s t : Set α) [DecidablePred (· ∈ s)] : (s ∪ t : Set α) ⊕ (s ∩ t : Set α) ≃ s ⊕ t

Full source

/-- If `s` is a set with decidable membership, then the sum of `s ∪ t` and `s ∩ t` is equivalent
to `s ⊕ t`. -/
protected def unionSumInter {α : Type u} (s t : Set α) [DecidablePred (· ∈ s)] :
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α)(s ∪ t : Set α) ⊕ (s ∩ t : Set α) ≃ s ⊕ t :=
  calc
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α)
      ≃ (s ∪ t \ s : Set α) ⊕ (s ∩ t : Set α) := by rw [union_diff_self]
    _ ≃ (s ⊕ (t \ s : Set α)) ⊕ (s ∩ t : Set α)calc
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α)
      ≃ (s ∪ t \ s : Set α) ⊕ (s ∩ t : Set α) := by rw [union_diff_self]
    _ ≃ (s ⊕ (t \ s : Set α)) ⊕ (s ∩ t : Set α) :=
      sumCongr (Set.union disjoint_sdiff_self_right) (Equiv.refl _)
    _ ≃ s ⊕ ((t \ s : Set α) ⊕ (s ∩ t : Set α))calc
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α)
      ≃ (s ∪ t \ s : Set α) ⊕ (s ∩ t : Set α) := by rw [union_diff_self]
    _ ≃ (s ⊕ (t \ s : Set α)) ⊕ (s ∩ t : Set α) :=
      sumCongr (Set.union disjoint_sdiff_self_right) (Equiv.refl _)
    _ ≃ s ⊕ ((t \ s : Set α) ⊕ (s ∩ t : Set α)) := sumAssoc _ _ _
    _ ≃ s ⊕ (t \ s ∪ s ∩ t : Set α)calc
    (s ∪ t : Set α) ⊕ (s ∩ t : Set α)
      ≃ (s ∪ t \ s : Set α) ⊕ (s ∩ t : Set α) := by rw [union_diff_self]
    _ ≃ (s ⊕ (t \ s : Set α)) ⊕ (s ∩ t : Set α) :=
      sumCongr (Set.union disjoint_sdiff_self_right) (Equiv.refl _)
    _ ≃ s ⊕ ((t \ s : Set α) ⊕ (s ∩ t : Set α)) := sumAssoc _ _ _
    _ ≃ s ⊕ (t \ s ∪ s ∩ t : Set α) :=
      sumCongr (Equiv.refl _)
        (by
          refine (Set.union' (· ∉ s) ?_ ?_).symm
          exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1])
    _ ≃ s ⊕ t := by
      { rw [(_ : t \ st \ s ∪ s ∩ t = t)]
        rw [union_comm, inter_comm, inter_union_diff] }

Equivalence between sum of union and intersection and sum of sets

Informal description

Given two sets $s$ and $t$ in a type $\alpha$ with a decidable membership predicate for $s$, the sum of the union $s \cup t$ and the intersection $s \cap t$ is equivalent to the sum of $s$ and $t$ as types. This equivalence is constructed by first rewriting the union as $s \cup (t \setminus s)$, then using the equivalence between disjoint unions and sums, and finally simplifying the expression to $s \oplus t$.

Equiv.Set.compl definition

 {α : Type u} {β : Type v} {s : Set α} {t : Set β} [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] (e₀ : s ≃ t) :
  { e : α ≃ β // ∀ x : s, e x = e₀ x } ≃ ((sᶜ : Set α) ≃ (tᶜ : Set β))

Full source

/-- Given an equivalence `e₀` between sets `s : Set α` and `t : Set β`, the set of equivalences
`e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences
between `sᶜ` and `tᶜ`. -/
protected def compl {α : Type u} {β : Type v} {s : Set α} {t : Set β} [DecidablePred (· ∈ s)]
    [DecidablePred (· ∈ t)] (e₀ : s ≃ t) :
    { e : α ≃ β // ∀ x : s, e x = e₀ x }{ e : α ≃ β // ∀ x : s, e x = e₀ x } ≃ ((sᶜ : Set α) ≃ (tᶜ : Set β)) where
  toFun e :=
    subtypeEquiv e fun _ =>
      not_congr <|
        Iff.symm <|
          MapsTo.mem_iff (mapsTo_iff_exists_map_subtype.2 ⟨e₀, e.2⟩)
            (SurjOn.mapsTo_compl
              (surjOn_iff_exists_map_subtype.2 ⟨t, e₀, Subset.refl t, e₀.surjective, e.2⟩)
              e.1.injective)
  invFun e₁ :=
    Subtype.mk
      (calc
        α ≃ s ⊕ (sᶜ : Set α) := (Set.sumCompl s).symm
        _ ≃ t ⊕ (tᶜ : Set β)calc
        α ≃ s ⊕ (sᶜ : Set α) := (Set.sumCompl s).symm
        _ ≃ t ⊕ (tᶜ : Set β) := e₀.sumCongr e₁
        _ ≃ β := Set.sumCompl t
        )
      fun x => by
      simp only [Sum.map_inl, trans_apply, sumCongr_apply, Set.sumCompl_apply_inl,
        Set.sumCompl_symm_apply, Trans.trans]
  left_inv e := by
    ext x
    by_cases hx : x ∈ s
    · simp only [Set.sumCompl_symm_apply_of_mem hx, ← e.prop ⟨x, hx⟩, Sum.map_inl, sumCongr_apply,
        trans_apply, Subtype.coe_mk, Set.sumCompl_apply_inl, Trans.trans]
    · simp only [Set.sumCompl_symm_apply_of_not_mem hx, Sum.map_inr, subtypeEquiv_apply,
        Set.sumCompl_apply_inr, trans_apply, sumCongr_apply, Subtype.coe_mk, Trans.trans]
  right_inv e :=
    Equiv.ext fun x => by
      simp only [Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, Function.comp_apply,
        sumCongr_apply, Equiv.coe_trans, Subtype.coe_eta, Subtype.coe_mk, Trans.trans,
        Set.sumCompl_symm_apply_compl]

Equivalence extension to complements

Informal description

Given types $\alpha$ and $\beta$, subsets $s \subseteq \alpha$ and $t \subseteq \beta$ with decidable membership predicates, and an equivalence $e_0$ between $s$ and $t$, the set of equivalences $e : \alpha \simeq \beta$ that extend $e_0$ (i.e., satisfy $e(x) = e_0(x)$ for all $x \in s$) is equivalent to the set of equivalences between the complements $s^c$ and $t^c$. More precisely, the equivalence is constructed as follows: - The forward map takes an equivalence $e$ extending $e_0$ and restricts it to the complements. - The inverse map combines $e_0$ with an equivalence between the complements to produce an equivalence on the whole types.

Equiv.Set.prod definition

{α β} (s : Set α) (t : Set β) : ↥(s ×ˢ t) ≃ s × t

Full source

/-- The set product of two sets is equivalent to the type product of their coercions to types. -/
protected def prod {α β} (s : Set α) (t : Set β) : ↥(s ×ˢ t) ≃ s × t :=
  @subtypeProdEquivProd α β s t

Equivalence between product set and product type of subsets

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the product set $s \times t$ is equivalent (as a type) to the product type of the subtypes corresponding to $s$ and $t$.

Equiv.Set.univPi definition

{α : Type*} {β : α → Type*} (s : ∀ a, Set (β a)) : pi univ s ≃ ∀ a, s a

Full source

/-- The set `Set.pi Set.univ s` is equivalent to `Π a, s a`. -/
@[simps]
protected def univPi {α : Type*} {β : α → Type*} (s : ∀ a, Set (β a)) :
    pipi univ s ≃ ∀ a, s a where
  toFun f a := ⟨(f : ∀ a, β a) a, f.2 a (mem_univ a)⟩
  invFun f := ⟨fun a => f a, fun a _ => (f a).2⟩
  left_inv := fun ⟨f, hf⟩ => by
    ext a
    rfl
  right_inv f := by
    ext a
    rfl

Equivalence between product set and dependent function type

Informal description

The set $\prod_{a \in \text{univ}} s(a)$ is equivalent to the type $\prod a, s(a)$, where $s(a)$ is a family of sets indexed by $a$. More precisely, the equivalence is given by: - The forward map takes a function $f$ in the product set and returns the function $\lambda a, \langle f(a), \text{proof that } f(a) \in s(a) \rangle$. - The inverse map takes a function $g$ in $\prod a, s(a)$ and returns the pair $\langle \lambda a, g(a), \text{proof that } g(a) \in s(a) \text{ for all } a \rangle$. This establishes a bijection between the set of functions in the product set and the dependent function type.

Equiv.Set.imageOfInjOn definition

{α β} (f : α → β) (s : Set α) (H : InjOn f s) : s ≃ f '' s

Full source

/-- If a function `f` is injective on a set `s`, then `s` is equivalent to `f '' s`. -/
protected noncomputable def imageOfInjOn {α β} (f : α → β) (s : Set α) (H : InjOn f s) :
    s ≃ f '' s :=
  ⟨fun p => ⟨f p, mem_image_of_mem f p.2⟩, fun p =>
    ⟨Classical.choose p.2, (Classical.choose_spec p.2).1⟩, fun ⟨_, h⟩ =>
    Subtype.eq
      (H (Classical.choose_spec (mem_image_of_mem f h)).1 h
        (Classical.choose_spec (mem_image_of_mem f h)).2),
    fun ⟨_, h⟩ => Subtype.eq (Classical.choose_spec h).2⟩

Bijection between a set and its image under an injective function

Informal description

Given a function $f : \alpha \to \beta$ and a subset $s \subseteq \alpha$, if $f$ is injective on $s$, then $s$ is in bijection with its image $f(s) \subseteq \beta$.

Equiv.Set.image definition

{α β} (f : α → β) (s : Set α) (H : Injective f) : s ≃ f '' s

Full source

/-- If `f` is an injective function, then `s` is equivalent to `f '' s`. -/
@[simps! apply]
protected noncomputable def image {α β} (f : α → β) (s : Set α) (H : Injective f) : s ≃ f '' s :=
  Equiv.Set.imageOfInjOn f s H.injOn

Bijection between a set and its image under an injective function

Informal description

Given an injective function $ f : \alpha \to \beta $ and a subset $ s \subseteq \alpha $, the set $ s $ is in bijection with its image $ f(s) \subseteq \beta $. More precisely, the equivalence is given by: - The forward map sends each $ x \in s $ to $ f(x) \in f(s) $. - The inverse map sends each $ y \in f(s) $ to the unique $ x \in s $ such that $ f(x) = y $ (which exists and is unique by injectivity of $ f $).

Equiv.Set.image_symm_apply theorem

 {α β} (f : α → β) (s : Set α) (H : Injective f) (x : α) (h : f x ∈ f '' s) :
  (Set.image f s H).symm ⟨f x, h⟩ = ⟨x, H.mem_set_image.1 h⟩

Full source

@[simp]
protected theorem image_symm_apply {α β} (f : α → β) (s : Set α) (H : Injective f) (x : α)
    (h : f x ∈ f '' s) : (Set.image f s H).symm ⟨f x, h⟩ = ⟨x, H.mem_set_image.1 h⟩ :=
  (Equiv.symm_apply_eq _).2 rfl

Inverse Image of Bijection Maps Back to Original Point

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s \subseteq \alpha$ a subset. For any $x \in \alpha$ such that $f(x) \in f(s)$, the inverse of the bijection between $s$ and $f(s)$ maps $\langle f(x), h \rangle$ back to $\langle x, H.\text{mem\_set\_image}.1 h \rangle$, where $h$ is the proof that $f(x) \in f(s)$.

Equiv.Set.image_symm_preimage theorem

 {α β} {f : α → β} (hf : Injective f) (u s : Set α) :
  (fun x => (Set.image f s hf).symm x : f '' s → α) ⁻¹' u = Subtype.val ⁻¹' (f '' u)

Full source

theorem image_symm_preimage {α β} {f : α → β} (hf : Injective f) (u s : Set α) :
    (fun x => (Set.image f s hf).symm x : f '' s → α) ⁻¹' u = Subtype.valSubtype.val ⁻¹' (f '' u) := by
  ext ⟨b, a, has, rfl⟩
  simp [hf.eq_iff]

Preimage of Inverse Bijection Equals Preimage of Image

Informal description

Let $f : \alpha \to \beta$ be an injective function, and let $u, s \subseteq \alpha$ be subsets. The preimage of $u$ under the inverse of the bijection between $s$ and $f(s)$ is equal to the preimage of $f(u)$ under the canonical projection from $f(s)$ to $\beta$. More precisely, for the inverse map $(f|_s)^{-1} : f(s) \to s$ of the bijection $s \simeq f(s)$, we have: $$(f|_s)^{-1}\ \text{⁻¹'}\ u = \text{Subtype.val}\ \text{⁻¹'}\ f(u)$$ where $\text{Subtype.val} : f(s) \to \beta$ is the inclusion map.

Equiv.Set.congr definition

{α β : Type*} (e : α ≃ β) : Set α ≃ Set β

Full source

/-- If `α` is equivalent to `β`, then `Set α` is equivalent to `Set β`. -/
@[simps]
protected def congr {α β : Type*} (e : α ≃ β) : SetSet α ≃ Set β :=
  ⟨fun s => e '' s, fun t => e.symm '' t, symm_image_image e, symm_image_image e.symm⟩

Equivalence of power sets induced by an equivalence of types

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, there is an induced equivalence between their power sets $\text{Set } \alpha$ and $\text{Set } \beta$. The forward map sends a subset $s \subseteq \alpha$ to its image $e(s) \subseteq \beta$, and the inverse map sends a subset $t \subseteq \beta$ to its preimage $e^{-1}(t) \subseteq \alpha$.

Equiv.Set.sep definition

{α : Type u} (s : Set α) (t : α → Prop) : ({x ∈ s | t x} : Set α) ≃ {x : s | t x}

Full source

/-- The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`. -/
protected def sep {α : Type u} (s : Set α) (t : α → Prop) :
    ({ x ∈ s | t x } : Set α) ≃ { x : s | t x } :=
  (Equiv.subtypeSubtypeEquivSubtypeInter s t).symm

Equivalence between a separated set and its subtype

Informal description

For any type $\alpha$, set $s \subseteq \alpha$, and predicate $t$ on $\alpha$, the set $\{x \in s \mid t(x)\}$ is equivalent (as a type) to the subtype $\{x : s \mid t(x)\}$ of elements of $s$ satisfying $t$.

Equiv.Set.powerset definition

{α} (S : Set α) : 𝒫 S ≃ Set S

Full source

/-- The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `Set S`. -/
protected def powerset {α} (S : Set α) :
    𝒫 S𝒫 S ≃ Set S where
  toFun := fun x : 𝒫 S => Subtype.valSubtype.val ⁻¹' (x : Set α)
  invFun := fun x : Set S => ⟨Subtype.val '' x, by rintro _ ⟨a : S, _, rfl⟩; exact a.2⟩
  left_inv x := by ext y;exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩
  right_inv x := by ext; simp

Equivalence between powerset and subsets of a set

Informal description

For any type $\alpha$ and subset $S \subseteq \alpha$, the powerset $\mathcal{P}(S) = \{x \mid x \subseteq S\}$ is equivalent to the type of subsets of $S$ (i.e., $\text{Set } S$). The equivalence is given by: - The forward map takes a subset $x \in \mathcal{P}(S)$ to its preimage under the inclusion map $\text{Subtype.val} : S \to \alpha$. - The inverse map takes a subset $x \in \text{Set } S$ to the image of $x$ under the inclusion map $\text{Subtype.val} : S \to \alpha$.

Equiv.Set.rangeSplittingImageEquiv definition

{α β : Type*} (f : α → β) (s : Set (range f)) : rangeSplitting f '' s ≃ s

Full source

/-- If `s` is a set in `range f`,
then its image under `rangeSplitting f` is in bijection (via `f`) with `s`.
-/
@[simps]
noncomputable def rangeSplittingImageEquiv {α β : Type*} (f : α → β) (s : Set (range f)) :
    rangeSplittingrangeSplitting f '' srangeSplitting f '' s ≃ s where
  toFun x :=
    ⟨⟨f x, by simp⟩, by
      rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
      simpa [apply_rangeSplitting f] using m⟩
  invFun x := ⟨rangeSplitting f x, ⟨x, ⟨x.2, rfl⟩⟩⟩
  left_inv x := by
    rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
    simp [apply_rangeSplitting f]
  right_inv x := by simp [apply_rangeSplitting f]

Bijection between range splitting image and subset of range

Informal description

Given a function $f : \alpha \to \beta$ and a subset $s$ of the range of $f$, the image of $s$ under the range splitting of $f$ is in bijection with $s$ itself. More precisely, the bijection is constructed as follows: - The forward map takes an element $x$ in the image of $s$ under the range splitting of $f$ and returns the corresponding element in $s$ by applying $f$. - The inverse map takes an element $x$ in $s$ and returns its preimage under the range splitting of $f$.

Equiv.Set.rangeInl definition

(α β : Type*) : Set.range (Sum.inl : α → α ⊕ β) ≃ α

Full source

/-- Equivalence between the range of `Sum.inl : α → α ⊕ β` and `α`. -/
@[simps symm_apply_coe]
def rangeInl (α β : Type*) : Set.rangeSet.range (Sum.inl : α → α ⊕ β) ≃ α where
  toFun
  | ⟨.inl x, _⟩ => x
  | ⟨.inr _, h⟩ => False.elim <| by rcases h with ⟨x, h'⟩; cases h'
  invFun x := ⟨.inl x, mem_range_self _⟩
  left_inv := fun ⟨_, _, rfl⟩ => rfl
  right_inv _ := rfl

Equivalence between the range of left inclusion and the left type

Informal description

The equivalence between the range of the left inclusion map $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ and the type $\alpha$. Specifically, it maps an element $\langle \text{Sum.inl} x, h \rangle$ in the range of $\text{Sum.inl}$ to $x \in \alpha$, and its inverse maps $x \in \alpha$ to $\langle \text{Sum.inl} x, \text{mem\_range\_self} \rangle$.

Equiv.Set.rangeInl_apply_inl theorem

{α : Type*} (β : Type*) (x : α) : (rangeInl α β) ⟨.inl x, mem_range_self _⟩ = x

Full source

@[simp] lemma rangeInl_apply_inl {α : Type*} (β : Type*) (x : α) :
    (rangeInl α β) ⟨.inl x, mem_range_self _⟩ = x :=
  rfl

Application of `rangeInl` to left inclusion element yields $x$

Informal description

For any types $\alpha$ and $\beta$, and any element $x \in \alpha$, the equivalence `rangeInl` maps the pair $\langle \text{Sum.inl}(x), \text{mem\_range\_self}\rangle$ in the range of $\text{Sum.inl}$ to $x$.

Equiv.Set.rangeInr definition

(α β : Type*) : Set.range (Sum.inr : β → α ⊕ β) ≃ β

Full source

/-- Equivalence between the range of `Sum.inr : β → α ⊕ β` and `β`. -/
@[simps symm_apply_coe]
def rangeInr (α β : Type*) : Set.rangeSet.range (Sum.inr : β → α ⊕ β) ≃ β where
  toFun
  | ⟨.inl _, h⟩ => False.elim <| by rcases h with ⟨x, h'⟩; cases h'
  | ⟨.inr x, _⟩ => x
  invFun x := ⟨.inr x, mem_range_self _⟩
  left_inv := fun ⟨_, _, rfl⟩ => rfl
  right_inv _ := rfl

Equivalence between range of right inclusion and codomain

Informal description

The equivalence between the range of the right inclusion function $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ and the type $\beta$. Specifically, it maps any element $\langle \text{Sum.inr} x, \_ \rangle$ in the range to $x$, and its inverse maps any $x \in \beta$ to $\langle \text{Sum.inr} x, \text{mem\_range\_self} \_ \rangle$.

Equiv.Set.rangeInr_apply_inr theorem

(α : Type*) {β : Type*} (x : β) : (rangeInr α β) ⟨.inr x, mem_range_self _⟩ = x

Full source

@[simp] lemma rangeInr_apply_inr (α : Type*) {β : Type*} (x : β) :
    (rangeInr α β) ⟨.inr x, mem_range_self _⟩ = x :=
  rfl

Application of `rangeInr` to right inclusion element yields $x$

Informal description

For any types $\alpha$ and $\beta$, and any element $x \in \beta$, the equivalence `rangeInr` maps the pair $\langle \text{Sum.inr}(x), \text{mem\_range\_self}\rangle$ in the range of $\text{Sum.inr}$ to $x$.

Equiv.ofLeftInverse definition

 {α β : Sort _} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) : α ≃ range f

Full source

/-- If `f : α → β` has a left-inverse when `α` is nonempty, then `α` is computably equivalent to the
range of `f`.

While awkward, the `Nonempty α` hypothesis on `f_inv` and `hf` allows this to be used when `α` is
empty too. This hypothesis is absent on analogous definitions on stronger `Equiv`s like
`LinearEquiv.ofLeftInverse` and `RingEquiv.ofLeftInverse` as their typeclass assumptions
are already sufficient to ensure non-emptiness. -/
@[simps]
def ofLeftInverse {α β : Sort _} (f : α → β) (f_inv : Nonempty α → β → α)
    (hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) :
    α ≃ range f where
  toFun a := ⟨f a, a, rfl⟩
  invFun b := f_inv (nonempty_of_exists b.2) b
  left_inv a := hf ⟨a⟩ a
  right_inv := fun ⟨b, a, ha⟩ =>
    Subtype.eq <| show f (f_inv ⟨a⟩ b) = b from Eq.trans (congr_arg f <| ha ▸ hf _ a) ha

Equivalence from left inverse to range

Informal description

Given a function $f : \alpha \to \beta$ and a partial left inverse $f_{\text{inv}}$ of $f$ (defined when $\alpha$ is nonempty), such that for any proof $h$ that $\alpha$ is nonempty, $f_{\text{inv}} h$ is a left inverse of $f$, then $\alpha$ is computably equivalent to the range of $f$. The equivalence maps $a \in \alpha$ to $\langle f(a), \exists a', f(a') = f(a) \rangle$ in the range, and its inverse maps $\langle b, \exists a, f(a) = b \rangle$ back to $f_{\text{inv}} h b$ where $h$ is a proof that $\alpha$ is nonempty (which exists because $b$ is in the range of $f$).

Equiv.ofLeftInverse' abbrev

{α β : Sort _} (f : α → β) (f_inv : β → α) (hf : LeftInverse f_inv f) : α ≃ range f

Full source

/-- If `f : α → β` has a left-inverse, then `α` is computably equivalent to the range of `f`.

Note that if `α` is empty, no such `f_inv` exists and so this definition can't be used, unlike
the stronger but less convenient `ofLeftInverse`. -/
abbrev ofLeftInverse' {α β : Sort _} (f : α → β) (f_inv : β → α) (hf : LeftInverse f_inv f) :
    α ≃ range f :=
  ofLeftInverse f (fun _ => f_inv) fun _ => hf

Equivalence from Left Inverse to Range (Simplified Version)

Informal description

Given a function $f \colon \alpha \to \beta$ and a left inverse $f_{\text{inv}} \colon \beta \to \alpha$ of $f$ (i.e., $f_{\text{inv}} \circ f = \text{id}_\alpha$), then $\alpha$ is computably equivalent to the range of $f$. The equivalence maps $a \in \alpha$ to $(f(a), \exists a', f(a') = f(a))$ in the range, and its inverse maps $(b, \exists a, f(a) = b)$ back to $f_{\text{inv}}(b)$.

Equiv.ofInjective definition

{α β} (f : α → β) (hf : Injective f) : α ≃ range f

Full source

/-- If `f : α → β` is an injective function, then domain `α` is equivalent to the range of `f`. -/
@[simps! apply]
noncomputable def ofInjective {α β} (f : α → β) (hf : Injective f) : α ≃ range f :=
  Equiv.ofLeftInverse f (fun _ => Function.invFun f) fun _ => Function.leftInverse_invFun hf

Equivalence between domain and range of an injective function

Informal description

Given an injective function $ f : \alpha \to \beta $, the domain $ \alpha $ is noncomputably equivalent to the range of $ f $. The equivalence maps each $ a \in \alpha $ to $ \langle f(a), \exists a', f(a') = f(a) \rangle $ in the range, and its inverse maps each $ \langle b, \exists a, f(a) = b \rangle $ back to the unique $ a \in \alpha $ such that $ f(a) = b $.

Equiv.apply_ofInjective_symm theorem

{α β} {f : α → β} (hf : Injective f) (b : range f) : f ((ofInjective f hf).symm b) = b

Full source

theorem apply_ofInjective_symm {α β} {f : α → β} (hf : Injective f) (b : range f) :
    f ((ofInjective f hf).symm b) = b :=
  Subtype.ext_iff.1 <| (ofInjective f hf).apply_symm_apply b

Inverse of injective equivalence preserves function application

Informal description

For any injective function $f \colon \alpha \to \beta$ and any element $b$ in the range of $f$, applying $f$ to the preimage of $b$ under the equivalence $\text{ofInjective}\,f\,hf$ yields $b$ again, i.e., $f((\text{ofInjective}\,f\,hf)^{-1}(b)) = b$.

Equiv.ofInjective_symm_apply theorem

{α β} {f : α → β} (hf : Injective f) (a : α) : (ofInjective f hf).symm ⟨f a, ⟨a, rfl⟩⟩ = a

Full source

@[simp]
theorem ofInjective_symm_apply {α β} {f : α → β} (hf : Injective f) (a : α) :
    (ofInjective f hf).symm ⟨f a, ⟨a, rfl⟩⟩ = a := by
  apply (ofInjective f hf).injective
  simp [apply_ofInjective_symm hf]

Inverse of injective equivalence preserves preimage

Informal description

Let $f : \alpha \to \beta$ be an injective function. For any $a \in \alpha$, the inverse of the equivalence $\text{ofInjective}\,f\,hf$ applied to the pair $\langle f(a), \langle a, \text{rfl}\rangle \rangle$ equals $a$, i.e., $$(\text{ofInjective}\,f\,hf)^{-1}\langle f(a), \langle a, \text{rfl}\rangle \rangle = a.$$

Equiv.coe_ofInjective_symm theorem

{α β} {f : α → β} (hf : Injective f) : ((ofInjective f hf).symm : range f → α) = rangeSplitting f

Full source

theorem coe_ofInjective_symm {α β} {f : α → β} (hf : Injective f) :
    ((ofInjective f hf).symm : range f → α) = rangeSplitting f := by
  ext ⟨y, x, rfl⟩
  apply hf
  simp [apply_rangeSplitting f]

Inverse of injective equivalence equals range-splitting function

Informal description

For any injective function $f \colon \alpha \to \beta$, the inverse of the equivalence $\text{ofInjective}\,f\,hf$ (as a function from the range of $f$ to $\alpha$) is equal to the range-splitting function of $f$, i.e., $$(\text{ofInjective}\,f\,hf)^{-1} = \text{rangeSplitting}\,f.$$

Equiv.self_comp_ofInjective_symm theorem

{α β} {f : α → β} (hf : Injective f) : f ∘ (ofInjective f hf).symm = Subtype.val

Full source

@[simp]
theorem self_comp_ofInjective_symm {α β} {f : α → β} (hf : Injective f) :
    f ∘ (ofInjective f hf).symm = Subtype.val :=
  funext fun x => apply_ofInjective_symm hf x

Composition of Function with Inverse Equivalence Yields Inclusion

Informal description

For any injective function $f \colon \alpha \to \beta$, the composition of $f$ with the inverse of the equivalence $\text{ofInjective}\,f\,hf$ equals the inclusion map from the range of $f$ back to $\beta$, i.e., $$ f \circ (\text{ofInjective}\,f\,hf)^{-1} = \text{Subtype.val}. $$

Equiv.ofLeftInverse_eq_ofInjective theorem

 {α β : Type*} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) :
  ofLeftInverse f f_inv hf =
    ofInjective f ((isEmpty_or_nonempty α).elim (fun _ _ _ _ => Subsingleton.elim _ _) (fun h => (hf h).injective))

Full source

theorem ofLeftInverse_eq_ofInjective {α β : Type*} (f : α → β) (f_inv : Nonempty α → β → α)
    (hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) :
    ofLeftInverse f f_inv hf =
      ofInjective f ((isEmpty_or_nonempty α).elim (fun _ _ _ _ => Subsingleton.elim _ _)
        (fun h => (hf h).injective)) := by
  ext
  simp

Equivalence from Left Inverse Equals Equivalence from Injectivity

Informal description

Let $f : \alpha \to \beta$ be a function between types $\alpha$ and $\beta$, and let $f_{\text{inv}} : \text{Nonempty } \alpha \to \beta \to \alpha$ be a partial left inverse of $f$ (defined when $\alpha$ is nonempty). Suppose that for every proof $h$ that $\alpha$ is nonempty, $f_{\text{inv}} h$ is a left inverse of $f$. Then the equivalence $\text{ofLeftInverse } f f_{\text{inv}} hf$ constructed from this data is equal to the equivalence $\text{ofInjective } f hf'$, where $hf'$ is the proof that $f$ is injective derived from the left inverse property when $\alpha$ is nonempty, and uses subsingleton elimination when $\alpha$ is empty.

Equiv.ofLeftInverse'_eq_ofInjective theorem

 {α β : Type*} (f : α → β) (f_inv : β → α) (hf : LeftInverse f_inv f) :
  ofLeftInverse' f f_inv hf = ofInjective f hf.injective

Full source

theorem ofLeftInverse'_eq_ofInjective {α β : Type*} (f : α → β) (f_inv : β → α)
    (hf : LeftInverse f_inv f) : ofLeftInverse' f f_inv hf = ofInjective f hf.injective := by
  ext
  simp

Equivalence from Left Inverse Equals Equivalence from Injectivity

Informal description

Given a function $f \colon \alpha \to \beta$ and a left inverse $f_{\text{inv}} \colon \beta \to \alpha$ of $f$ (i.e., $f_{\text{inv}} \circ f = \text{id}_\alpha$), the equivalence $\text{ofLeftInverse'}\, f\, f_{\text{inv}}\, hf$ constructed from this data is equal to the equivalence $\text{ofInjective}\, f\, hf_{\text{inj}}$, where $hf_{\text{inj}}$ is the proof that $f$ is injective derived from the left inverse property.

Equiv.set_forall_iff theorem

{α β} (e : α ≃ β) {p : Set α → Prop} : (∀ a, p a) ↔ ∀ a, p (e ⁻¹' a)

Full source

protected theorem set_forall_iff {α β} (e : α ≃ β) {p : Set α → Prop} :
    (∀ a, p a) ↔ ∀ a, p (e ⁻¹' a) :=
  e.injective.preimage_surjective.forall

Universal Quantifier Preservation under Equivalence via Preimage

Informal description

Let $e : \alpha \simeq \beta$ be an equivalence between types $\alpha$ and $\beta$. For any predicate $p$ on subsets of $\alpha$, the statement $(\forall a \subseteq \alpha, p(a))$ holds if and only if $(\forall a \subseteq \beta, p(e^{-1}(a)))$ holds.

Equiv.preimage_piEquivPiSubtypeProd_symm_pi theorem

 {α : Type*} {β : α → Type*} (p : α → Prop) [DecidablePred p] (s : ∀ i, Set (β i)) :
  (piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s =
    (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i

Full source

theorem preimage_piEquivPiSubtypeProd_symm_pi {α : Type*} {β : α → Type*} (p : α → Prop)
    [DecidablePred p] (s : ∀ i, Set (β i)) :
    (piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s =
      (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i := by
  ext ⟨f, g⟩
  simp only [mem_preimage, mem_univ_pi, prodMk_mem_set_prod_eq, Subtype.forall, ← forall_and]
  refine forall_congr' fun i => ?_
  dsimp only [Subtype.coe_mk]
  by_cases hi : p i <;> simp [hi]

Preimage of Product Set under Subtype-Product Equivalence

Informal description

Let $\alpha$ be a type and $\beta \colon \alpha \to \text{Type}$ be a family of types indexed by $\alpha$. Given a decidable predicate $p$ on $\alpha$ and a family of sets $s_i \subseteq \beta_i$ for each $i \in \alpha$, the preimage of the product set $\prod_{i \in \alpha} s_i$ under the inverse of the equivalence $\text{piEquivPiSubtypeProd}\, p\, \beta$ is equal to the Cartesian product of the product sets $\prod_{i \in \{j \mid p j\}} s_i$ and $\prod_{i \in \{j \mid \neg p j\}} s_i$.

Equiv.sigmaPreimageEquiv definition

{α β} (f : α → β) : (Σ b, f ⁻¹' { b }) ≃ α

Full source

/-- `sigmaPreimageEquiv f` for `f : α → β` is the natural equivalence between
the type of all preimages of points under `f` and the total space `α`. -/
@[simps!]
def sigmaPreimageEquiv {α β} (f : α → β) : (Σb, f ⁻¹' {b}) ≃ α :=
  sigmaFiberEquiv f

Equivalence between preimage sigma type and domain

Informal description

For any function $f : \alpha \to \beta$, the natural equivalence between the type of all preimages of points under $f$ (represented as a dependent pair type $\Sigma b, f^{-1}(\{b\})$) and the total space $\alpha$.

Equiv.ofPreimageEquiv definition

{α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, f ⁻¹' { c } ≃ g ⁻¹' { c }) : α ≃ β

Full source

/-- A family of equivalences between preimages of points gives an equivalence between domains. -/
@[simps!]
def ofPreimageEquiv {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, f ⁻¹' {c}f ⁻¹' {c} ≃ g ⁻¹' {c}) : α ≃ β :=
  Equiv.ofFiberEquiv e

Equivalence from fiberwise equivalences

Informal description

Given functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, and a family of equivalences $e_c \colon f^{-1}(\{c\}) \simeq g^{-1}(\{c\})$ between their fibers for each $c \in \gamma$, there exists an equivalence $\alpha \simeq \beta$ that respects these fiber equivalences.

Equiv.ofPreimageEquiv_map theorem

 {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, f ⁻¹' { c } ≃ g ⁻¹' { c }) (a : α) : g (ofPreimageEquiv e a) = f a

Full source

theorem ofPreimageEquiv_map {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, f ⁻¹' {c}f ⁻¹' {c} ≃ g ⁻¹' {c})
    (a : α) : g (ofPreimageEquiv e a) = f a :=
  Equiv.ofFiberEquiv_map e a

Commutativity of `Equiv.ofPreimageEquiv` with respect to $f$ and $g$

Informal description

Given functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, and a family of equivalences $e_c \colon f^{-1}(\{c\}) \simeq g^{-1}(\{c\})$ between their fibers for each $c \in \gamma$, the equivalence $\alpha \simeq \beta$ constructed via `Equiv.ofPreimageEquiv` satisfies $g(e(a)) = f(a)$ for any $a \in \alpha$.

Set.BijOn.equiv definition

{α : Type*} {β : Type*} {s : Set α} {t : Set β} (f : α → β) (h : BijOn f s t) : s ≃ t

Full source

/-- If a function is a bijection between two sets `s` and `t`, then it induces an
equivalence between the types `↥s` and `↥t`. -/
noncomputable def Set.BijOn.equiv {α : Type*} {β : Type*} {s : Set α} {t : Set β} (f : α → β)
    (h : BijOn f s t) : s ≃ t :=
  Equiv.ofBijective _ h.bijective

Equivalence induced by a bijection on sets

Informal description

Given a function $f : \alpha \to \beta$ that is a bijection between two sets $s \subseteq \alpha$ and $t \subseteq \beta$, there exists an equivalence (bijective correspondence) between the subtypes $s$ and $t$ induced by $f$.

dite_comp_equiv_update theorem

 {α : Type*} {β : Sort*} {γ : Sort*} {p : α → Prop} (e : β ≃ { x // p x }) (v : β → γ) (w : α → γ) (j : β) (x : γ)
  [DecidableEq β] [DecidableEq α] [∀ j, Decidable (p j)] :
  (fun i : α => if h : p i then (Function.update v j x) (e.symm ⟨i, h⟩) else w i) =
    Function.update (fun i : α => if h : p i then v (e.symm ⟨i, h⟩) else w i) (e j) x

Full source

/-- The composition of an updated function with an equiv on a subtype can be expressed as an
updated function. -/
theorem dite_comp_equiv_update {α : Type*} {β : Sort*} {γ : Sort*} {p : α → Prop}
    (e : β ≃ {x // p x})
    (v : β → γ) (w : α → γ) (j : β) (x : γ) [DecidableEq β] [DecidableEq α]
    [∀ j, Decidable (p j)] :
    (fun i : α => if h : p i then (Function.update v j x) (e.symm ⟨i, h⟩) else w i) =
      Function.update (fun i : α => if h : p i then v (e.symm ⟨i, h⟩) else w i) (e j) x := by
  ext i
  by_cases h : p i
  · rw [dif_pos h, Function.update_apply_equiv_apply, Equiv.symm_symm,
      Function.update_apply, Function.update_apply, dif_pos h]
    have h_coe : (⟨i, h⟩ : Subtype p) = e j ↔ i = e j :=
      Subtype.ext_iff.trans (by rw [Subtype.coe_mk])
    simp [h_coe]
  · have : i ≠ e j := by
      contrapose! h
      have : p (e j : α) := (e j).2
      rwa [← h] at this
    simp [h, this]

Equality of Updated Composition with Equivalence and Updated Conditional Function

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, and let $p \colon \alpha \to \text{Prop}$ be a predicate on $\alpha$. Given an equivalence $e \colon \beta \simeq \{x \in \alpha \mid p x\}$, functions $v \colon \beta \to \gamma$ and $w \colon \alpha \to \gamma$, an element $j \in \beta$, and a value $x \in \gamma$, the following equality holds: \[ \left(\lambda i \in \alpha, \begin{cases} \text{update } v \, j \, x \, (e^{-1}\langle i, h \rangle) & \text{if } h \colon p i, \\ w i & \text{otherwise} \end{cases}\right) = \text{update } \left(\lambda i \in \alpha, \begin{cases} v (e^{-1}\langle i, h \rangle) & \text{if } h \colon p i, \\ w i & \text{otherwise} \end{cases}\right) \, (e j) \, x \] Here, $\text{update}$ denotes the function update operation, and $e^{-1}$ is the inverse of the equivalence $e$.

Equiv.swap_bijOn_self theorem

(hs : a ∈ s ↔ b ∈ s) : BijOn (Equiv.swap a b) s s

Full source

theorem Equiv.swap_bijOn_self (hs : a ∈ sa ∈ s ↔ b ∈ s) : BijOn (Equiv.swap a b) s s := by
  refine ⟨fun x hx ↦ ?_, (Equiv.injective _).injOn, fun x hx ↦ ?_⟩
  · obtain (rfl | hxa) := eq_or_ne x a
    · rwa [swap_apply_left, ← hs]
    obtain (rfl | hxb) := eq_or_ne x b
    · rwa [swap_apply_right, hs]
    rwa [swap_apply_of_ne_of_ne hxa hxb]
  obtain (rfl | hxa) := eq_or_ne x a
  · simp [hs.1 hx]
  obtain (rfl | hxb) := eq_or_ne x b
  · simp [hs.2 hx]
  exact ⟨x, hx, swap_apply_of_ne_of_ne hxa hxb⟩

Bijectivity of Swap Function on Self-Mapping Set

Informal description

For any two distinct elements $a$ and $b$ of a type and a set $s$, if $a$ is in $s$ if and only if $b$ is in $s$, then the swap function $\text{swap}(a, b)$ is a bijection from $s$ to itself.

Equiv.swap_bijOn_exchange theorem

(ha : a ∈ s) (hb : b ∉ s) : BijOn (Equiv.swap a b) s (insert b (s \ { a }))

Full source

theorem Equiv.swap_bijOn_exchange (ha : a ∈ s) (hb : b ∉ s) :
    BijOn (Equiv.swap a b) s (insert b (s \ {a})) := by
  refine ⟨fun x hx ↦ ?_, (Equiv.injective _).injOn, fun x hx ↦ ?_⟩
  · obtain (rfl | hxa) := eq_or_ne x a
    · simp [swap_apply_left]
    rw [swap_apply_of_ne_of_ne hxa (by rintro rfl; contradiction)]
    exact .inr ⟨hx, hxa⟩
  obtain (rfl | hxb) := eq_or_ne x b
  · exact ⟨a, ha, by simp⟩
  simp only [mem_insert_iff, mem_diff, mem_singleton_iff, or_iff_right hxb] at hx
  exact ⟨x, hx.1, swap_apply_of_ne_of_ne hx.2 hxb⟩

Bijectivity of Swap Function on Set Exchange

Informal description

Let $a$ and $b$ be distinct elements of a type, and let $s$ be a set such that $a \in s$ and $b \notin s$. Then the function $\text{swap}(a, b)$, which swaps $a$ and $b$, is a bijection from $s$ to the set obtained by inserting $b$ and removing $a$ from $s$, i.e., $s \mapsto \{b\} \cup (s \setminus \{a\})$.