# Equivalence between types #

In this file we continue the work on equivalences begun in `Mathlib/Logic/Equiv/Defs.lean`, defining a lot of equivalences between various types and operations on these equivalences.

More definitions of this kind can be found in other files. E.g., `Mathlib/Algebra/Equiv/TransferInstance.lean` does it for many algebraic type classes like `Group`, `Module`, etc.

## Tags #

equivalence, congruence, bijective map

source
def Equiv.piOptionEquivProd {α : Type u_10} {β : Option α → Type u_9} :
((a : Option α) → β a) ≃ β none × ((a : α) → β (some a))

The product over `Option α` of `β a` is the binary product of the product over `α` of `β (some α)` and `β none`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.piOptionEquivProd_apply {α : Type u_10} {β : Option α → Type u_9} (f : (a : Option α) → β a) :
piOptionEquivProd f = (f none, fun (a : α) => f (some a))
source
@[simp]
theorem Equiv.piOptionEquivProd_symm_apply {α : Type u_10} {β : Option α → Type u_9} (x : β none × ((a : α) → β (some a))) (a : Option α) :
piOptionEquivProd.symm x a = Option.casesOn a x.fst x.snd
source
def Equiv.subtypeCongr {α : Type u_9} {p q : α → Prop} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } ≃ { x : α // q x }) (f : { x : α // ¬p x } ≃ { x : α // ¬q x }) :
Perm α

Combines an `Equiv` between two subtypes with an `Equiv` between their complements to form a permutation.

Equations

- e.subtypeCongr f = (Equiv.sumCompl p).symm.trans ((e.sumCongr f).trans (Equiv.sumCompl q))

Instances For

source
def Equiv.Perm.subtypeCongr {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) :
Perm ε

Combining permutations on `ε` that permute only inside or outside the subtype split induced by `p : ε → Prop` constructs a permutation on `ε`.

Equations

- ep.subtypeCongr en = (Equiv.sumCompl p).permCongr (ep.sumCongr en)

Instances For

source
theorem Equiv.Perm.subtypeCongr.apply {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) (a : ε) :
(ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)
source
@[simp]
theorem Equiv.Perm.subtypeCongr.left_apply {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) {a : ε} (h : p a) :
(ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)
source
@[simp]
theorem Equiv.Perm.subtypeCongr.left_apply_subtype {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) (a : { a : ε // p a }) :
(ep.subtypeCongr en) ↑a = ↑(ep a)
source
@[simp]
theorem Equiv.Perm.subtypeCongr.right_apply {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) {a : ε} (h : ¬p a) :
(ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)
source
@[simp]
theorem Equiv.Perm.subtypeCongr.right_apply_subtype {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) (a : { a : ε // ¬p a }) :
(ep.subtypeCongr en) ↑a = ↑(en a)
source
@[simp]
theorem Equiv.Perm.subtypeCongr.refl {ε : Type u_9} {p : ε → Prop} [DecidablePred p] :
subtypeCongr (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) = Equiv.refl ε
source
@[simp]
theorem Equiv.Perm.subtypeCongr.symm {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) :
Equiv.symm (ep.subtypeCongr en) = subtypeCongr (Equiv.symm ep) (Equiv.symm en)
source
@[simp]
theorem Equiv.Perm.subtypeCongr.trans {ε : Type u_9} {p : ε → Prop} [DecidablePred p] (ep ep' : Perm { a : ε // p a }) (en en' : Perm { a : ε // ¬p a }) :
Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')
source
def Equiv.subtypePreimage {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a : α // p a } → β) :
{ x : α → β // x ∘ Subtype.val = x₀ } ≃ ({ a : α // ¬p a } → β)

For a fixed function `x₀ : {a // p a} → β` defined on a subtype of `α`, the subtype of functions `x : α → β` that agree with `x₀` on the subtype `{a // p a}` is naturally equivalent to the type of functions `{a // ¬ p a} → β`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.subtypePreimage_apply {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a : α // p a } → β) (x : { x : α → β // x ∘ Subtype.val = x₀ }) (a : { a : α // ¬p a }) :
(subtypePreimage p x₀) x a = ↑x ↑a
source
@[simp]
theorem Equiv.subtypePreimage_symm_apply_coe {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a : α // p a } → β) (x : { a : α // ¬p a } → β) (a : α) :
↑((subtypePreimage p x₀).symm x) a = if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩
source
theorem Equiv.subtypePreimage_symm_apply_coe_pos {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a : α // p a } → β) (x : { a : α // ¬p a } → β) (a : α) (h : p a) :
↑((subtypePreimage p x₀).symm x) a = x₀ ⟨a, h⟩
source
theorem Equiv.subtypePreimage_symm_apply_coe_neg {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a : α // p a } → β) (x : { a : α // ¬p a } → β) (a : α) (h : ¬p a) :
↑((subtypePreimage p x₀).symm x) a = x ⟨a, h⟩
source
def Equiv.piCongrRight {α : Sort u_1} {β₁ : α → Sort u_9} {β₂ : α → Sort u_10} (F : (a : α) → β₁ a ≃ β₂ a) :
((a : α) → β₁ a) ≃ ((a : α) → β₂ a)

A family of equivalences `∀ a, β₁ a ≃ β₂ a` generates an equivalence between `∀ a, β₁ a` and `∀ a, β₂ a`.

Equations

- Equiv.piCongrRight F = { toFun := Pi.map fun (a : α) => ⇑(F a), invFun := Pi.map fun (a : α) => ⇑(F a).symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.piCongrRight_symm_apply {α : Sort u_1} {β₁ : α → Sort u_9} {β₂ : α → Sort u_10} (F : (a : α) → β₁ a ≃ β₂ a) (a✝ : (i : α) → β₂ i) (i : α) :
(piCongrRight F).symm a✝ i = Pi.map (fun (a : α) => ⇑(F a).symm) a✝ i
source
@[simp]
theorem Equiv.piCongrRight_apply {α : Sort u_1} {β₁ : α → Sort u_9} {β₂ : α → Sort u_10} (F : (a : α) → β₁ a ≃ β₂ a) (a✝ : (i : α) → β₁ i) (i : α) :
(piCongrRight F) a✝ i = Pi.map (fun (a : α) => ⇑(F a)) a✝ i
source
@[simp]
theorem Equiv.piCongrRight_refl {α : Sort u_1} {β : α → Sort u_9} :
(piCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) → β a)
source
def Equiv.piComm {α : Sort u_1} {β : Sort u_4} (φ : α → β → Sort u_9) :
((a : α) → (b : β) → φ a b) ≃ ((b : β) → (a : α) → φ a b)

Given `φ : α → β → Sort*`, we have an equivalence between `∀ a b, φ a b` and `∀ b a, φ a b`. This is `Function.swap` as an `Equiv`.

Equations

- Equiv.piComm φ = { toFun := Function.swap, invFun := Function.swap, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.piComm_apply {α : Sort u_1} {β : Sort u_4} (φ : α → β → Sort u_9) (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :
(piComm φ) f y x = Function.swap f y x
source
@[simp]
theorem Equiv.piComm_symm {α : Sort u_1} {β : Sort u_4} {φ : α → β → Sort u_9} :
(piComm φ).symm = piComm (Function.swap φ)
source
def Equiv.piCurry {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) :
((x : (i : α) × β i) → γ x.fst x.snd) ≃ ((a : α) → (b : β a) → γ a b)

Dependent `curry` equivalence: the type of dependent functions on `Σ i, β i` is equivalent to the type of dependent functions of two arguments (i.e., functions to the space of functions).

This is `Sigma.curry` and `Sigma.uncurry` together as an equiv.

Equations

- Equiv.piCurry γ = { toFun := Sigma.curry, invFun := Sigma.uncurry, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.piCurry_apply {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (x : (i : α) × β i) → γ x.fst x.snd) :
(piCurry γ) f = Sigma.curry f
source
@[simp]
theorem Equiv.piCurry_symm_apply {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (a : α) → (b : β a) → γ a b) :
(piCurry γ).symm f = Sigma.uncurry f
source
def Equiv.ofFiberEquiv {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c }) :
α ≃ β

A family of equivalences between fibers gives an equivalence between domains.

Equations

- Equiv.ofFiberEquiv e = (Equiv.sigmaFiberEquiv f).symm.trans ((Equiv.sigmaCongrRight e).trans (Equiv.sigmaFiberEquiv g))

Instances For

source
@[simp]
theorem Equiv.ofFiberEquiv_symm_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c }) (a✝ : β) :
(ofFiberEquiv e).symm a✝ = ↑((sigmaCongrRight e).symm ((sigmaFiberEquiv g).symm a✝)).snd
source
@[simp]
theorem Equiv.ofFiberEquiv_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c }) (a✝ : α) :
(ofFiberEquiv e) a✝ = ↑((e (f a✝)) ((sigmaFiberEquiv f).symm a✝).snd)
source
theorem Equiv.ofFiberEquiv_map {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ} (e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c }) (a : α) :
g ((ofFiberEquiv e) a) = f a
source
def Equiv.sigmaNatSucc (f : ℕ → Type u) :
(n : ℕ) × f n ≃ f 0 ⊕ (n : ℕ) × f (n + 1)

An equivalence that separates out the 0th fiber of `(Σ (n : ℕ), f n)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.natEquivNatSumPUnit :
ℕ ≃ ℕ ⊕ PUnit.{u_9 + 1}

The set of natural numbers is equivalent to `ℕ ⊕ PUnit`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.natSumPUnitEquivNat :
ℕ ⊕ PUnit.{u_9 + 1} ≃ ℕ

`ℕ ⊕ PUnit` is equivalent to `ℕ`.

Equations

- Equiv.natSumPUnitEquivNat = Equiv.natEquivNatSumPUnit.symm

Instances For

source
def Equiv.intEquivNatSumNat :
ℤ ≃ ℕ ⊕ ℕ

The type of integer numbers is equivalent to `ℕ ⊕ ℕ`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.uniqueCongr {α : Sort u_1} {β : Sort u_4} (e : α ≃ β) :
Unique α ≃ Unique β

If `α` is equivalent to `β`, then `Unique α` is equivalent to `Unique β`.

Equations

- e.uniqueCongr = { toFun := fun (h : Unique α) => e.symm.unique, invFun := fun (h : Unique β) => e.unique, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
theorem Equiv.isEmpty_congr {α : Sort u_1} {β : Sort u_4} (e : α ≃ β) :
IsEmpty α ↔ IsEmpty β

If `α` is equivalent to `β`, then `IsEmpty α` is equivalent to `IsEmpty β`.

source
theorem Equiv.isEmpty {α : Sort u_1} {β : Sort u_4} (e : α ≃ β) [IsEmpty β] :
IsEmpty α
source
def Equiv.subtypeEquiv {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) :
{ a : α // p a } ≃ { b : β // q b }

If `α` is equivalent to `β` and the predicates `p : α → Prop` and `q : β → Prop` are equivalent at corresponding points, then `{a // p a}` is equivalent to `{b // q b}`. For the statement where `α = β`, that is, `e : perm α`, see `Perm.subtypePerm`.

Equations

- e.subtypeEquiv h = { toFun := fun (a : { a : α // p a }) => ⟨e ↑a, ⋯⟩, invFun := fun (b : { b : β // q b }) => ⟨e.symm ↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.subtypeEquiv_apply {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) (a : { a : α // p a }) :
(e.subtypeEquiv h) a = ⟨e ↑a, ⋯⟩
source
theorem Equiv.coe_subtypeEquiv_eq_map {X : Sort u_9} {Y : Sort u_10} {p : X → Prop} {q : Y → Prop} (e : X ≃ Y) (h : ∀ (x : X), p x ↔ q (e x)) :
⇑(e.subtypeEquiv h) = Subtype.map ⇑e ⋯
source
@[simp]
theorem Equiv.subtypeEquiv_refl {α : Sort u_1} {p : α → Prop} (h : ∀ (a : α), p a ↔ p ((Equiv.refl α) a) := ⋯) :
(Equiv.refl α).subtypeEquiv h = Equiv.refl { a : α // p a }
source
@[simp]
theorem Equiv.subtypeEquiv_symm {α : Sort u_1} {β : Sort u_4} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) :
(e.subtypeEquiv h).symm = e.symm.subtypeEquiv ⋯
source
@[simp]
theorem Equiv.subtypeEquiv_trans {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {p : α → Prop} {q : β → Prop} {r : γ → Prop} (e : α ≃ β) (f : β ≃ γ) (h : ∀ (a : α), p a ↔ q (e a)) (h' : ∀ (b : β), q b ↔ r (f b)) :
(e.subtypeEquiv h).trans (f.subtypeEquiv h') = (e.trans f).subtypeEquiv ⋯
source
def Equiv.subtypeEquivRight {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) :
{ x : α // p x } ≃ { x : α // q x }

If two predicates `p` and `q` are pointwise equivalent, then `{x // p x}` is equivalent to `{x // q x}`.

Equations

- Equiv.subtypeEquivRight e = (Equiv.refl α).subtypeEquiv e

Instances For

source
@[simp]
theorem Equiv.subtypeEquivRight_apply_coe {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (a : { a : α // p a }) :
↑((subtypeEquivRight e) a) = ↑a
source
@[simp]
theorem Equiv.subtypeEquivRight_symm_apply_coe {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (b : { b : α // q b }) :
↑((subtypeEquivRight e).symm b) = ↑b
source
theorem Equiv.subtypeEquivRight_apply {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x : α // p x }) :
(subtypeEquivRight e) z = ⟨↑z, ⋯⟩
source
theorem Equiv.subtypeEquivRight_symm_apply {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x : α // q x }) :
(subtypeEquivRight e).symm z = ⟨↑z, ⋯⟩
source
def Equiv.subtypeEquivOfSubtype {α : Sort u_1} {β : Sort u_4} {p : β → Prop} (e : α ≃ β) :
{ a : α // p (e a) } ≃ { b : β // p b }

If `α ≃ β`, then for any predicate `p : β → Prop` the subtype `{a // p (e a)}` is equivalent to the subtype `{b // p b}`.

Equations

- e.subtypeEquivOfSubtype = e.subtypeEquiv ⋯

Instances For

source
def Equiv.subtypeEquivOfSubtype' {α : Sort u_1} {β : Sort u_4} {p : α → Prop} (e : α ≃ β) :
{ a : α // p a } ≃ { b : β // p (e.symm b) }

If `α ≃ β`, then for any predicate `p : α → Prop` the subtype `{a // p a}` is equivalent to the subtype `{b // p (e.symm b)}`. This version is used by `equiv_rw`.

Equations

- e.subtypeEquivOfSubtype' = e.symm.subtypeEquivOfSubtype.symm

Instances For

source
def Equiv.subtypeEquivProp {α : Sort u_1} {p q : α → Prop} (h : p = q) :
Subtype p ≃ Subtype q

If two predicates are equal, then the corresponding subtypes are equivalent.

Equations

- Equiv.subtypeEquivProp h = (Equiv.refl α).subtypeEquiv ⋯

Instances For

source
def Equiv.subtypeSubtypeEquivSubtypeExists {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) :
Subtype q ≃ { a : α // ∃ (h : p a), q ⟨a, h⟩ }

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This version allows the “inner” predicate to depend on `h : p a`.

Equations

- Equiv.subtypeSubtypeEquivSubtypeExists p q = { toFun := fun (a : Subtype q) => ⟨↑↑a, ⋯⟩, invFun := fun (a : { a : α // ∃ (h : p a), q ⟨a, h⟩ }) => ⟨⟨↑a, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : { a : α // ∃ (h : p a), q ⟨a, h⟩ }) :
↑↑((subtypeSubtypeEquivSubtypeExists p q).symm a) = ↑a
source
@[simp]
theorem Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : Subtype q) :
↑((subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a
source
def Equiv.subtypeSubtypeEquivSubtypeInter {α : Type u} (p q : α → Prop) :
{ x : Subtype p // q ↑x } ≃ { x : α // p x ∧ q x }

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates.

Equations

- Equiv.subtypeSubtypeEquivSubtypeInter p q = (Equiv.subtypeSubtypeEquivSubtypeExists p fun (x : Subtype p) => q ↑x).trans (Equiv.subtypeEquivRight ⋯)

Instances For

source
@[simp]
theorem Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe {α : Type u} (p q : α → Prop) (a✝ : { x : Subtype p // q ↑x }) :
↑((subtypeSubtypeEquivSubtypeInter p q) a✝) = ↑↑a✝
source
@[simp]
theorem Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe {α : Type u} (p q : α → Prop) (a✝ : { x : α // p x ∧ q x }) :
↑↑((subtypeSubtypeEquivSubtypeInter p q).symm a✝) = ↑a✝
source
def Equiv.subtypeSubtypeEquivSubtype {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) :
{ x : Subtype p // q ↑x } ≃ Subtype q

If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.

Equations

- Equiv.subtypeSubtypeEquivSubtype h = (Equiv.subtypeSubtypeEquivSubtypeInter p q).trans (Equiv.subtypeEquivRight ⋯)

Instances For

source
@[simp]
theorem Equiv.subtypeSubtypeEquivSubtype_apply_coe {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) (a✝ : { x : Subtype p // q ↑x }) :
↑((subtypeSubtypeEquivSubtype h) a✝) = ↑↑a✝
source
@[simp]
theorem Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) (a✝ : Subtype q) :
↑↑((subtypeSubtypeEquivSubtype h).symm a✝) = ↑a✝
source
def Equiv.subtypeUnivEquiv {α : Type u_9} {p : α → Prop} (h : ∀ (x : α), p x) :
Subtype p ≃ α

If a proposition holds for all elements, then the subtype is equivalent to the original type.

Equations

- Equiv.subtypeUnivEquiv h = { toFun := fun (x : Subtype p) => ↑x, invFun := fun (x : α) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.subtypeUnivEquiv_apply {α : Type u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : Subtype p) :
(subtypeUnivEquiv h) x = ↑x
source
@[simp]
theorem Equiv.subtypeUnivEquiv_symm_apply {α : Type u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) :
(subtypeUnivEquiv h).symm x = ⟨x, ⋯⟩
source
def Equiv.subtypeSigmaEquiv {α : Type u_9} (p : α → Type v) (q : α → Prop) :
{ y : Sigma p // q y.fst } ≃ (x : Subtype q) × p ↑x

A subtype of a sigma-type is a sigma-type over a subtype.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.sigmaSubtypeEquivOfSubset {α : Type u_9} (p : α → Type v) (q : α → Prop) (h : ∀ (x : α) (a : p x), q x) :
(x : Subtype q) × p ↑x ≃ (x : α) × p x

A sigma type over a subtype is equivalent to the sigma set over the original type, if the fiber is empty outside of the subset

Equations

- Equiv.sigmaSubtypeEquivOfSubset p q h = (Equiv.subtypeSigmaEquiv p q).symm.trans (Equiv.subtypeUnivEquiv ⋯)

Instances For

source
def Equiv.sigmaSubtypeFiberEquiv {α : Type u_9} {β : Type u_10} (f : α → β) (p : β → Prop) (h : ∀ (x : α), p (f x)) :
(y : Subtype p) × { x : α // f x = ↑y } ≃ α

If a predicate `p : β → Prop` is true on the range of a map `f : α → β`, then `Σ y : {y // p y}, {x // f x = y}` is equivalent to `α`.

Equations

- Equiv.sigmaSubtypeFiberEquiv f p h = Trans.trans (Equiv.sigmaSubtypeEquivOfSubset (fun (y : β) => { x : α // f x = y }) p ⋯) (Equiv.sigmaFiberEquiv f)

Instances For

source
def Equiv.sigmaSubtypeFiberEquivSubtype {α : Type u_9} {β : Type u_10} (f : α → β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (f x)) :
(y : Subtype q) × { x : α // f x = ↑y } ≃ Subtype p

If for each `x` we have `p x ↔ q (f x)`, then `Σ y : {y // q y}, f ⁻¹' {y}` is equivalent to `{x // p x}`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.sigmaOptionEquivOfSome {α : Type u_9} (p : Option α → Type v) (h : ∀ (a : p none), False) :
(x : Option α) × p x ≃ (x : α) × p (some x)

A sigma type over an `Option` is equivalent to the sigma set over the original type, if the fiber is empty at none.

Equations

- Equiv.sigmaOptionEquivOfSome p h = (Equiv.sigmaSubtypeEquivOfSubset p (fun (x : Option α) => x.isSome = true) ⋯).symm.trans (Equiv.optionIsSomeEquiv α).sigmaCongrLeft'

Instances For

source
def Equiv.piEquivSubtypeSigma (ι : Type u_10) (π : ι → Type u_9) :
((i : ι) → π i) ≃ { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst = i }

The `Pi`-type `∀ i, π i` is equivalent to the type of sections `f : ι → Σ i, π i` of the `Sigma` type such that for all `i` we have `(f i).fst = i`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.subtypePiEquivPi {α : Sort u_1} {β : α → Sort v} {p : (a : α) → β a → Prop} :
{ f : (a : α) → β a // ∀ (a : α), p a (f a) } ≃ ((a : α) → { b : β a // p a b })

The type of functions `f : ∀ a, β a` such that for all `a` we have `p a (f a)` is equivalent to the type of functions `∀ a, {b : β a // p a b}`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Equiv.sigmaAssocProd {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} :
(ab : α × β) × γ ab.fst ab.snd ≃ (a : α) × (b : β) × γ a b

A sigma of a sigma whose second base does not depend on the first is equivalent to a sigma whose base is a product.

Equations

- Equiv.sigmaAssocProd = (Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft'.trans (Equiv.sigmaAssoc γ)

Instances For

source
@[simp]
theorem Equiv.sigmaAssocProd_apply_fst {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.fst a.snd) :
(sigmaAssocProd a✝).fst = ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.fst
source
@[simp]
theorem Equiv.sigmaAssocProd_symm_apply_fst {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α) × (b : β) × γ a b) :
(sigmaAssocProd.symm a✝).fst = (((sigmaAssoc γ).symm a✝).fst.fst, ((sigmaAssoc γ).symm a✝).fst.snd)
source
@[simp]
theorem Equiv.sigmaAssocProd_apply_snd_fst {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.fst a.snd) :
(sigmaAssocProd a✝).snd.fst = ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.snd
source
@[simp]
theorem Equiv.sigmaAssocProd_symm_apply_snd {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α) × (b : β) × γ a b) :
(sigmaAssocProd.symm a✝).snd = ((sigmaAssoc γ).symm a✝).snd
source
@[simp]
theorem Equiv.sigmaAssocProd_apply_snd_snd {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.fst a.snd) :
(sigmaAssocProd a✝).snd.snd = ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).snd
source
def Equiv.sigmaSubtype {α : Type u_9} {β : α → Type u_10} (a : α) :
{ s : Sigma β // s.fst = a } ≃ β a

A subtype of a sigma which pins down the base of the sigma is equivalent to the respective fiber.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.sigmaSubtype_symm_apply_coe_fst {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) :
(↑((sigmaSubtype a).symm b)).fst = a
source
@[simp]
theorem Equiv.sigmaSubtype_apply {α : Type u_9} {β : α → Type u_10} (a : α) (x✝ : { s : Sigma β // s.fst = a }) :
(sigmaSubtype a) x✝ = match x✝ with | ⟨⟨fst, b⟩, h⟩ => h ▸ b
source
@[simp]
theorem Equiv.sigmaSubtype_symm_apply_coe_snd {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) :
(↑((sigmaSubtype a).symm b)).snd = b
source
def Equiv.sigmaSigmaSubtype {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop) [uniq : Unique { ab : (a : α) × β a // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩) :
{ s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ } ≃ γ a b

A subtype of a dependent triple which pins down both bases is equivalent to the respective fiber.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.sigmaSigmaSubtype_apply {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop) [uniq : Unique { ab : (a : α) × β a // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩) (a✝ : { s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ }) :
(sigmaSigmaSubtype p h) a✝ = cast ⋯ (↑a✝).snd.snd
source
@[simp]
theorem Equiv.sigmaSigmaSubtype_symm_apply {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop) [uniq : Unique { ab : (a : α) × β a // p ab }] {a : α} {b : β a} (c : γ a b) (h : p ⟨a, b⟩) :
(sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩
source
def Equiv.sigmaSigmaSubtypeEq {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : α) (b : β) :
{ s : (a : α) × (b : β) × γ a b // s.fst = a ∧ s.snd.fst = b } ≃ γ a b

A specialization of `sigmaSigmaSubtype` to the case where the second base does not depend on the first, and the property being checked for is simple equality. Useful e.g. when `γ` is `Hom` inside a category.

Equations

- Equiv.sigmaSigmaSubtypeEq a b = Equiv.sigmaSigmaSubtype (fun (x : (_ : α) × β) => match x with | ⟨a', b'⟩ => a' = a ∧ b' = b) ⋯

Instances For

source
@[simp]
theorem Equiv.sigmaSigmaSubtypeEq_apply {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (s : { s : (a : α) × (b : β) × γ a b // s.fst = a ∧ s.snd.fst = b }) :
(sigmaSigmaSubtypeEq a b) s = cast ⋯ (↑s).snd.snd
source
@[simp]
theorem Equiv.sigmaSigmaSubtypeEq_symm_apply {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (c : γ a b) :
(sigmaSigmaSubtypeEq a b).symm c = ⟨⟨a, ⟨b, c⟩⟩, ⋯⟩
source
def Equiv.subtypeEquivCodomain {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) :
{ g : X → Y // g ∘ Subtype.val = f } ≃ Y

The type of all functions `X → Y` with prescribed values for all `x' ≠ x` is equivalent to the codomain `Y`.

Equations

- Equiv.subtypeEquivCodomain f = (Equiv.subtypePreimage (fun (a : X) => a ≠ x) f).trans (Equiv.funUnique { x' : X // ¬x' ≠ x } Y)

Instances For

source
@[simp]
theorem Equiv.coe_subtypeEquivCodomain {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) :
⇑(subtypeEquivCodomain f) = fun (g : { g : X → Y // g ∘ Subtype.val = f }) => ↑g x
source
@[simp]
theorem Equiv.subtypeEquivCodomain_apply {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) (g : { g : X → Y // g ∘ Subtype.val = f }) :
(subtypeEquivCodomain f) g = ↑g x
source
theorem Equiv.coe_subtypeEquivCodomain_symm {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) :
⇑(subtypeEquivCodomain f).symm = fun (y : Y) => ⟨fun (x' : X) => if h : x' ≠ x then f ⟨x', h⟩ else y, ⋯⟩
source
@[simp]
theorem Equiv.subtypeEquivCodomain_symm_apply {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) (y : Y) (x' : X) :
↑((subtypeEquivCodomain f).symm y) x' = if h : x' ≠ x then f ⟨x', h⟩ else y
source
theorem Equiv.subtypeEquivCodomain_symm_apply_eq {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) (y : Y) :
↑((subtypeEquivCodomain f).symm y) x = y
source
theorem Equiv.subtypeEquivCodomain_symm_apply_ne {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' ≠ x } → Y) (y : Y) (x' : X) (h : x' ≠ x) :
↑((subtypeEquivCodomain f).symm y) x' = f ⟨x', h⟩
source
instance Equiv.instCanLiftForallCoeBijective {α : Sort u_1} {β : Sort u_4} :
CanLift (α → β) (α ≃ β) DFunLike.coe Function.Bijective
source
def Equiv.Perm.extendDomain {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) :
Perm β'

Extend the domain of `e : Equiv.Perm α` to one that is over `β` via `f : α → Subtype p`, where `p : β → Prop`, permuting only the `b : β` that satisfy `p b`. This can be used to extend the domain across a function `f : α → β`, keeping everything outside of `Set.range f` fixed. For this use-case `Equiv` given by `f` can be constructed by `Equiv.of_leftInverse'` or `Equiv.of_leftInverse` when there is a known inverse, or `Equiv.ofInjective` in the general case.

Equations

- e.extendDomain f = (f.permCongr e).subtypeCongr (Equiv.refl { a : β' // ¬p a })

Instances For

source
@[simp]
theorem Equiv.Perm.extendDomain_apply_image {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) (a : α') :
(e.extendDomain f) ↑(f a) = ↑(f (e a))
source
theorem Equiv.Perm.extendDomain_apply_subtype {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) {b : β'} (h : p b) :
(e.extendDomain f) b = ↑(f (e (f.symm ⟨b, h⟩)))
source
theorem Equiv.Perm.extendDomain_apply_not_subtype {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) {b : β'} (h : ¬p b) :
(e.extendDomain f) b = b
source
@[simp]
theorem Equiv.Perm.extendDomain_refl {α' : Type u_9} {β' : Type u_10} {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) :
extendDomain (Equiv.refl α') f = Equiv.refl β'
source
@[simp]
theorem Equiv.Perm.extendDomain_symm {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) :
Equiv.symm (e.extendDomain f) = extendDomain (Equiv.symm e) f
source
theorem Equiv.Perm.extendDomain_trans {α' : Type u_9} {β' : Type u_10} {p : β' → Prop} [DecidablePred p] (f : α' ≃ Subtype p) (e e' : Perm α') :
Equiv.trans (e.extendDomain f) (e'.extendDomain f) = extendDomain (Equiv.trans e e') f
source
def Equiv.subtypeQuotientEquivQuotientSubtype {α : Sort u_1} (p₁ : α → Prop) {s₁ : Setoid α} {s₂ : Setoid (Subtype p₁)} (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y) :
{ x : Quotient s₁ // p₂ x } ≃ Quotient s₂

Subtype of the quotient is equivalent to the quotient of the subtype. Let `α` be a setoid with equivalence relation `~`. Let `p₂` be a predicate on the quotient type `α/~`, and `p₁` be the lift of this predicate to `α`: `p₁ a ↔ p₂ ⟦a⟧`. Let `~₂` be the restriction of `~` to `{x // p₁ x}`. Then `{x // p₂ x}` is equivalent to the quotient of `{x // p₁ x}` by `~₂`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.subtypeQuotientEquivQuotientSubtype_mk {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ ↑x ≈ ↑y) (x : α) (hx : p₂ ⟦x⟧) :
(subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) ⟨⟦x⟧, hx⟩ = ⟦⟨x, ⋯⟩⟧
source
@[simp]
theorem Equiv.subtypeQuotientEquivQuotientSubtype_symm_mk {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ ↑x ≈ ↑y) (x : Subtype p₁) :
(subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm ⟦x⟧ = ⟨⟦↑x⟧, ⋯⟩
source
def Equiv.swapCore {α : Sort u_1} [DecidableEq α] (a b r : α) :
α

A helper function for `Equiv.swap`.

Equations

- Equiv.swapCore a b r = if r = a then b else if r = b then a else r

Instances For

source
theorem Equiv.swapCore_self {α : Sort u_1} [DecidableEq α] (r a : α) :
swapCore a a r = r
source
theorem Equiv.swapCore_swapCore {α : Sort u_1} [DecidableEq α] (r a b : α) :
swapCore a b (swapCore a b r) = r
source
theorem Equiv.swapCore_comm {α : Sort u_1} [DecidableEq α] (r a b : α) :
swapCore a b r = swapCore b a r
source
def Equiv.swap {α : Sort u_1} [DecidableEq α] (a b : α) :
Perm α

`swap a b` is the permutation that swaps `a` and `b` and leaves other values as is.

Equations

- Equiv.swap a b = { toFun := Equiv.swapCore a b, invFun := Equiv.swapCore a b, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.swap_self {α : Sort u_1} [DecidableEq α] (a : α) :
swap a a = Equiv.refl α
source
theorem Equiv.swap_comm {α : Sort u_1} [DecidableEq α] (a b : α) :
swap a b = swap b a
source
theorem Equiv.swap_apply_def {α : Sort u_1} [DecidableEq α] (a b x : α) :
(swap a b) x = if x = a then b else if x = b then a else x
source
@[simp]
theorem Equiv.swap_apply_left {α : Sort u_1} [DecidableEq α] (a b : α) :
(swap a b) a = b
source
@[simp]
theorem Equiv.swap_apply_right {α : Sort u_1} [DecidableEq α] (a b : α) :
(swap a b) b = a
source
theorem Equiv.swap_apply_of_ne_of_ne {α : Sort u_1} [DecidableEq α] {a b x : α} :
x ≠ a → x ≠ b → (swap a b) x = x
source
theorem Equiv.eq_or_eq_of_swap_apply_ne_self {α : Sort u_1} [DecidableEq α] {a b x : α} (h : (swap a b) x ≠ x) :
x = a ∨ x = b
source
@[simp]
theorem Equiv.swap_swap {α : Sort u_1} [DecidableEq α] (a b : α) :
Equiv.trans (swap a b) (swap a b) = Equiv.refl α
source
@[simp]
theorem Equiv.symm_swap {α : Sort u_1} [DecidableEq α] (a b : α) :
Equiv.symm (swap a b) = swap a b
source
@[simp]
theorem Equiv.swap_eq_refl_iff {α : Sort u_1} [DecidableEq α] {x y : α} :
swap x y = Equiv.refl α ↔ x = y
source
theorem Equiv.swap_comp_apply {α : Sort u_1} [DecidableEq α] {a b x : α} (π : Perm α) :
(Equiv.trans π (swap a b)) x = if π x = a then b else if π x = b then a else π x
source
theorem Equiv.swap_eq_update {α : Sort u_1} [DecidableEq α] (i j : α) :
⇑(swap i j) = Function.update (Function.update id j i) i j
source
theorem Equiv.comp_swap_eq_update {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (i j : α) (f : α → β) :
f ∘ ⇑(swap i j) = Function.update (Function.update f j (f i)) i (f j)
source
@[simp]
theorem Equiv.symm_trans_swap_trans {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (a b : α) (e : α ≃ β) :
(e.symm.trans (swap a b)).trans e = swap (e a) (e b)
source
@[simp]
theorem Equiv.trans_swap_trans_symm {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (a b : β) (e : α ≃ β) :
(e.trans (swap a b)).trans e.symm = swap (e.symm a) (e.symm b)
source
@[simp]
theorem Equiv.swap_apply_self {α : Sort u_1} [DecidableEq α] (i j a : α) :
(swap i j) ((swap i j) a) = a
source
theorem Equiv.apply_swap_eq_self {α : Sort u_1} {β : Sort u_4} [DecidableEq α] {v : α → β} {i j : α} (hv : v i = v j) (k : α) :
v ((swap i j) k) = v k

A function is invariant to a swap if it is equal at both elements

source
theorem Equiv.swap_apply_eq_iff {α : Sort u_1} [DecidableEq α] {x y z w : α} :
(swap x y) z = w ↔ z = (swap x y) w
source
theorem Equiv.swap_apply_ne_self_iff {α : Sort u_1} [DecidableEq α] {a b x : α} :
(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
source
@[simp]
theorem Equiv.Perm.sumCongr_swap_refl {α : Type u_9} {β : Type u_10} [DecidableEq α] [DecidableEq β] (i j : α) :
(swap i j).sumCongr (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)
source
@[simp]
theorem Equiv.Perm.sumCongr_refl_swap {α : Type u_9} {β : Type u_10} [DecidableEq α] [DecidableEq β] (i j : β) :
sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)
source
def Equiv.setValue {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (f : α ≃ β) (a : α) (b : β) :
α ≃ β

Augment an equivalence with a prescribed mapping `f a = b`

Equations

- f.setValue a b = Equiv.trans (Equiv.swap a (f.symm b)) f

Instances For

source
@[simp]
theorem Equiv.setValue_eq {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (f : α ≃ β) (a : α) (b : β) :
(f.setValue a b) a = b
source
def Function.Involutive.toPerm {α : Sort u_1} (f : α → α) (h : Involutive f) :
Equiv.Perm α

Convert an involutive function `f` to a permutation with `toFun = invFun = f`.

Equations

- Function.Involutive.toPerm f h = { toFun := f, invFun := f, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Function.Involutive.coe_toPerm {α : Sort u_1} {f : α → α} (h : Involutive f) :
⇑(toPerm f h) = f
source
@[simp]
theorem Function.Involutive.toPerm_symm {α : Sort u_1} {f : α → α} (h : Involutive f) :
Equiv.symm (toPerm f h) = toPerm f h
source
theorem Function.Involutive.toPerm_involutive {α : Sort u_1} {f : α → α} (h : Involutive f) :
Involutive ⇑(toPerm f h)
source
theorem Function.Involutive.symm_eq_self_of_involutive {α : Sort u_1} (f : Equiv.Perm α) (h : Involutive ⇑f) :
Equiv.symm f = f
source
theorem PLift.eq_up_iff_down_eq {α : Sort u_1} {x : PLift α} {y : α} :
x = { down := y } ↔ x.down = y
source
theorem Function.Injective.map_swap {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Injective f) (x y z : α) :
f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
source
def Equiv.piCongrLeft' {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) :
((a : α) → P a) ≃ ((b : β) → P (e.symm b))

Transport dependent functions through an equivalence of the base space.

Equations

- Equiv.piCongrLeft' P e = { toFun := fun (f : (a : α) → P a) (x : β) => f (e.symm x), invFun := fun (f : (b : β) → P (e.symm b)) (x : α) => ⋯ ▸ f (e x), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.piCongrLeft'_apply {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (f : (a : α) → P a) (x : β) :
(piCongrLeft' P e) f x = f (e.symm x)
source
theorem Equiv.piCongrLeft'_symm_apply {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (f : (b : β) → P (e.symm b)) (x : α) :
(piCongrLeft' P e).symm f x = ⋯ ▸ f (e x)

Note: the "obvious" statement `(piCongrLeft' P e).symm g a = g (e a)` doesn't typecheck: the LHS would have type `P a` while the RHS would have type `P (e.symm (e a))`. For that reason, we have to explicitly substitute along `e.symm (e a) = a` in the statement of this lemma.

source
@[simp]
theorem Equiv.piCongrLeft'_symm {α : Sort u_1} {β : Sort u_4} (P : Sort u_9) (e : α ≃ β) :
(piCongrLeft' (fun (x : α) => P) e).symm = piCongrLeft' (fun (a : β) => P) e.symm

This lemma is impractical to state in the dependent case.

source
@[simp]
theorem Equiv.piCongrLeft'_symm_apply_apply {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (g : (b : β) → P (e.symm b)) (b : β) :
(piCongrLeft' P e).symm g (e.symm b) = g b

Note: the "obvious" statement `(piCongrLeft' P e).symm g a = g (e a)` doesn't typecheck: the LHS would have type `P a` while the RHS would have type `P (e.symm (e a))`. This lemma is a way around it in the case where `a` is of the form `e.symm b`, so we can use `g b` instead of `g (e (e.symm b))`.

source
@[simp]
theorem Equiv.piCongrLeft'_refl {α : Sort u_1} (P : α → Sort u_9) :
piCongrLeft' P (Equiv.refl α) = Equiv.refl ((a : α) → P a)
source
def Equiv.piCongrLeft {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) :
((a : α) → P (e a)) ≃ ((b : β) → P b)

Transporting dependent functions through an equivalence of the base, expressed as a "simplification".

Equations

- Equiv.piCongrLeft P e = (Equiv.piCongrLeft' P e.symm).symm

Instances For

source
theorem Equiv.piCongrLeft_apply {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (b : β) :
(piCongrLeft P e) f b = ⋯ ▸ f (e.symm b)

Note: the "obvious" statement `(piCongrLeft P e) f b = f (e.symm b)` doesn't typecheck: the LHS would have type `P b` while the RHS would have type `P (e (e.symm b))`. For that reason, we have to explicitly substitute along `e (e.symm b) = b` in the statement of this lemma.

source
@[simp]
theorem Equiv.piCongrLeft_symm_apply {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (g : (b : β) → P b) (a : α) :
(piCongrLeft P e).symm g a = g (e a)
source
@[simp]
theorem Equiv.piCongrLeft_refl {α : Sort u_1} (P : α → Sort u_9) :
piCongrLeft P (Equiv.refl α) = Equiv.refl ((a : α) → P a)
source
@[simp]
theorem Equiv.piCongrLeft_apply_apply {α : Sort u_1} {β : Sort u_4} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (a : α) :
(piCongrLeft P e) f (e a) = f a

Note: the "obvious" statement `(piCongrLeft P e) f b = f (e.symm b)` doesn't typecheck: the LHS would have type `P b` while the RHS would have type `P (e (e.symm b))`. This lemma is a way around it in the case where `b` is of the form `e a`, so we can use `f a` instead of `f (e.symm (e a))`.

source
theorem Equiv.piCongrLeft_apply_eq_cast {α : Sort u_1} {β : Sort u_4} {P : β → Sort v} {e : α ≃ β} (f : (a : α) → P (e a)) (b : β) :
(piCongrLeft P e) f b = cast ⋯ (f (e.symm b))
source
theorem Equiv.piCongrLeft_sumInl {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι'' → Type u_9) (e : ι ⊕ ι' ≃ ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (i : ι) :
(piCongrLeft π e) ((sumPiEquivProdPi fun (x : ι ⊕ ι') => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i
source
theorem Equiv.piCongrLeft_sumInr {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι'' → Type u_9) (e : ι ⊕ ι' ≃ ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (j : ι') :
(piCongrLeft π e) ((sumPiEquivProdPi fun (x : ι ⊕ ι') => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j
source
def Equiv.piCongr {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a)) :
((a : α) → W a) ≃ ((b : β) → Z b)

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibers.

Equations

- h₁.piCongr h₂ = (Equiv.piCongrRight h₂).trans (Equiv.piCongrLeft Z h₁)

Instances For

source
@[simp]
theorem Equiv.coe_piCongr_symm {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a)) :
⇑(h₁.piCongr h₂).symm = fun (f : (b : β) → Z b) (a : α) => (h₂ a).symm (f (h₁ a))
source
@[simp]
theorem Equiv.piCongr_symm_apply {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a)) (f : (b : β) → Z b) :
(h₁.piCongr h₂).symm f = fun (a : α) => (h₂ a).symm (f (h₁ a))
source
@[simp]
theorem Equiv.piCongr_apply_apply {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a)) (f : (a : α) → W a) (a : α) :
(h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)
source
def Equiv.piCongr' {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b) :
((a : α) → W a) ≃ ((b : β) → Z b)

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibres.

Equations

- h₁.piCongr' h₂ = (h₁.symm.piCongr fun (b : β) => (h₂ b).symm).symm

Instances For

source
@[simp]
theorem Equiv.coe_piCongr' {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b) :
⇑(h₁.piCongr' h₂) = fun (f : (a : α) → W a) (b : β) => (h₂ b) (f (h₁.symm b))
source
theorem Equiv.piCongr'_apply {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b) (f : (a : α) → W a) :
(h₁.piCongr' h₂) f = fun (b : β) => (h₂ b) (f (h₁.symm b))
source
@[simp]
theorem Equiv.piCongr'_symm_apply_symm_apply {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b) (f : (b : β) → Z b) (b : β) :
(h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)
source
def Equiv.piCongrSet {α : Type u_9} {W : α → Sort w} {s t : Set α} (h : s = t) :
((i : { i : α // i ∈ s }) → W ↑i) ≃ ((i : { i : α // i ∈ t }) → W ↑i)

Transport dependent functions through an equality of sets.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.piCongrSet_apply {α : Type u_9} {W : α → Sort w} {s t : Set α} (h : s = t) (f : (i : { i : α // i ∈ s }) → W ↑i) (i : { i : α // i ∈ t }) :
(piCongrSet h) f i = f ⟨↑i, ⋯⟩
source
@[simp]
theorem Equiv.piCongrSet_symm_apply {α : Type u_9} {W : α → Sort w} {s t : Set α} (h : s = t) (f : (i : { i : α // i ∈ t }) → W ↑i) (i : { i : α // i ∈ s }) :
(piCongrSet h).symm f i = f ⟨↑i, ⋯⟩
source
theorem Equiv.eq_conj {α : Sort u_9} {α' : Sort u_10} {β : Sort u_11} {β' : Sort u_12} (ε₁ : α ≃ α') (ε₂ : β' ≃ β) (f : α → β) (f' : α' → β') :
⇑ε₂.symm ∘ f ∘ ⇑ε₁.symm = f' ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁
source
theorem Equiv.semiconj_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁) :
Function.Semiconj (⇑e) f (e.conj f)
source
theorem Equiv.semiconj₂_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) :
Function.Semiconj₂ (⇑e) f ((e.arrowCongr e.conj) f)
source
instance Equiv.instAssociativeCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.Associative f] :
Std.Associative ((e.arrowCongr (e.arrowCongr e)) f)
source
instance Equiv.instIdempotentOpCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.IdempotentOp f] :
Std.IdempotentOp ((e.arrowCongr (e.arrowCongr e)) f)
source
@[simp]
theorem Equiv.ulift_symm_down {α : Type v} (x : α) :
(Equiv.ulift.symm x).down = x
source
theorem Function.Injective.swap_apply {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Injective f) (x y z : α) :
(Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
source
theorem Function.Injective.swap_comp {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Injective f) (x y : α) :
⇑(Equiv.swap (f x) (f y)) ∘ f = f ∘ ⇑(Equiv.swap x y)
source
def equivOfSubsingletonOfSubsingleton {α : Sort u_1} {β : Sort u_4} [Subsingleton α] [Subsingleton β] (f : α → β) (g : β → α) :
α ≃ β

To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.

Equations

- equivOfSubsingletonOfSubsingleton f g = { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
noncomputable def Equiv.punitOfNonemptyOfSubsingleton {α : Sort u_1} [h : Nonempty α] [Subsingleton α] :
α ≃ PUnit.{u_9}

A nonempty subsingleton type is (noncomputably) equivalent to `PUnit`.

Equations

- Equiv.punitOfNonemptyOfSubsingleton = equivOfSubsingletonOfSubsingleton (fun (x : α) => PUnit.unit) fun (x : PUnit.{?u.16}) => h.some

Instances For

source
def uniqueUniqueEquiv {α : Sort u_1} :
Unique (Unique α) ≃ Unique α

`Unique (Unique α)` is equivalent to `Unique α`.

Equations

- uniqueUniqueEquiv = equivOfSubsingletonOfSubsingleton (fun (h : Unique (Unique α)) => default) fun (h : Unique α) => { default := h, uniq := ⋯ }

Instances For

source
def uniqueEquivEquivUnique (α : Sort u) (β : Sort v) [Unique β] :
Unique α ≃ (α ≃ β)

If `Unique β`, then `Unique α` is equivalent to `α ≃ β`.

Equations

- uniqueEquivEquivUnique α β = equivOfSubsingletonOfSubsingleton (fun (x : Unique α) => Equiv.ofUnique α β) Equiv.unique

Instances For

source
theorem Function.update_comp_equiv {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [DecidableEq α'] [DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) :
update f a v ∘ ⇑g = update (f ∘ ⇑g) (g.symm a) v
source
theorem Function.update_apply_equiv_apply {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [DecidableEq α'] [DecidableEq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) (a' : α') :
update f a v (g a') = update (f ∘ ⇑g) (g.symm a) v a'
source
theorem Function.piCongrLeft'_update {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (P : α → Sort u_10) (e : α ≃ β) (f : (a : α) → P a) (b : β) (x : P (e.symm b)) :
(Equiv.piCongrLeft' P e) (update f (e.symm b) x) = update ((Equiv.piCongrLeft' P e) f) b x
source
theorem Function.piCongrLeft'_symm_update {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (P : α → Sort u_10) (e : α ≃ β) (f : (b : β) → P (e.symm b)) (b : β) (x : P (e.symm b)) :
(Equiv.piCongrLeft' P e).symm (update f b x) = update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x