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

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.

@[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

@[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))

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))

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)

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⟩)

@[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⟩)

@[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)

@[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⟩)

@[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)

@[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 ε

@[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)

@[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')

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.

@[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⟩

@[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

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⟩

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⟩

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 := ⋯ }

@[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

@[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

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 := ⋯ }

@[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

@[simp]

theorem Equiv.piComm_symm {α : Sort u_1} {β : Sort u_4} {φ : α → β → Sort u_9} : (piComm φ).symm = piComm (Function.swap φ)

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 := ⋯ }

@[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

@[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

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))

@[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)

@[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

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

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.

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.

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

ℕ ⊕ PUnit is equivalent to ℕ.

Equations

• Equiv.natSumPUnitEquivNat = Equiv.natEquivNatSumPUnit.symm

def Equiv.intEquivNatSumNat : ℤ ≃ ℕ ⊕ ℕ

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

Equations

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

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 := ⋯ }

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

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

theorem Equiv.isEmpty {α : Sort u_1} {β : Sort u_4} (e : α ≃ β) [IsEmpty β] : IsEmpty α

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 := ⋯ }

@[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, ⋯⟩

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 ⋯

@[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 }

@[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 ⋯

@[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 ⋯

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

@[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

@[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

theorem Equiv.subtypeEquivRight_apply {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (z : { x : α // p x }) : (subtypeEquivRight e) z = ⟨↑z, ⋯⟩

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, ⋯⟩

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 ⋯

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

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 ⋯

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 := ⋯ }

@[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

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : Subtype q) : ↑((subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a

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 ⋯)

@[simp]

theorem Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe {α : Type u} (p q : α → Prop) (a✝ : { x : Subtype p // q ↑x }) : ↑((subtypeSubtypeEquivSubtypeInter p q) a✝) = ↑↑a✝

@[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✝

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 ⋯)

@[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✝

@[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✝

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 := ⋯ }

@[simp]

theorem Equiv.subtypeUnivEquiv_symm_apply {α : Type u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) : (subtypeUnivEquiv h).symm x = ⟨x, ⋯⟩

@[simp]

theorem Equiv.subtypeUnivEquiv_apply {α : Type u_9} {p : α → Prop} (h : ∀ (x : α), p x) (x : Subtype p) : (subtypeUnivEquiv h) x = ↑x

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.

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 ⋯)

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)

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.

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'

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.

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.

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 γ)

@[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

@[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

@[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

@[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

@[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)

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.

@[simp]

theorem Equiv.sigmaSubtype_symm_apply_coe_fst {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) : (↑((sigmaSubtype a).symm b)).fst = a

@[simp]

theorem Equiv.sigmaSubtype_symm_apply_coe_snd {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) : (↑((sigmaSubtype a).symm b)).snd = b

@[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

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.

@[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

@[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⟩

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) ⋯

@[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

@[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⟩⟩, ⋯⟩

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)

@[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

@[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

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, ⋯⟩

@[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

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

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⟩

instance Equiv.instCanLiftForallCoeBijective {α : Sort u_1} {β : Sort u_4} : CanLift (α → β) (α ≃ β) DFunLike.coe Function.Bijective

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 })

@[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))

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⟩)))

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

@[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 β'

@[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

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

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.

@[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, ⋯⟩⟧

@[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⟧, ⋯⟩

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

theorem Equiv.swapCore_self {α : Sort u_1} [DecidableEq α] (r a : α) : swapCore a a r = r

theorem Equiv.swapCore_swapCore {α : Sort u_1} [DecidableEq α] (r a b : α) : swapCore a b (swapCore a b r) = r

theorem Equiv.swapCore_comm {α : Sort u_1} [DecidableEq α] (r a b : α) : swapCore a b r = swapCore b a r

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 := ⋯ }

@[simp]

theorem Equiv.swap_self {α : Sort u_1} [DecidableEq α] (a : α) : swap a a = Equiv.refl α

theorem Equiv.swap_comm {α : Sort u_1} [DecidableEq α] (a b : α) : swap a b = swap b a

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

@[simp]

theorem Equiv.swap_apply_left {α : Sort u_1} [DecidableEq α] (a b : α) : (swap a b) a = b

@[simp]

theorem Equiv.swap_apply_right {α : Sort u_1} [DecidableEq α] (a b : α) : (swap a b) b = a

theorem Equiv.swap_apply_of_ne_of_ne {α : Sort u_1} [DecidableEq α] {a b x : α} : x ≠ a → x ≠ b → (swap a b) x = x

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

@[simp]

theorem Equiv.swap_swap {α : Sort u_1} [DecidableEq α] (a b : α) : Equiv.trans (swap a b) (swap a b) = Equiv.refl α

@[simp]

theorem Equiv.symm_swap {α : Sort u_1} [DecidableEq α] (a b : α) : Equiv.symm (swap a b) = swap a b

@[simp]

theorem Equiv.swap_eq_refl_iff {α : Sort u_1} [DecidableEq α] {x y : α} : swap x y = Equiv.refl α ↔ x = y

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

theorem Equiv.swap_eq_update {α : Sort u_1} [DecidableEq α] (i j : α) : ⇑(swap i j) = Function.update (Function.update id j i) i j

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)

@[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)

@[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)

@[simp]

theorem Equiv.swap_apply_self {α : Sort u_1} [DecidableEq α] (i j a : α) : (swap i j) ((swap i j) a) = a

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

theorem Equiv.swap_apply_eq_iff {α : Sort u_1} [DecidableEq α] {x y z w : α} : (swap x y) z = w ↔ z = (swap x y) w

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)

@[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)

@[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)

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

@[simp]

theorem Equiv.setValue_eq {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (f : α ≃ β) (a : α) (b : β) : (f.setValue a b) a = b

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 := ⋯ }

@[simp]

theorem Function.Involutive.coe_toPerm {α : Sort u_1} {f : α → α} (h : Involutive f) : ⇑(toPerm f h) = f

@[simp]

theorem Function.Involutive.toPerm_symm {α : Sort u_1} {f : α → α} (h : Involutive f) : Equiv.symm (toPerm f h) = toPerm f h

theorem Function.Involutive.toPerm_involutive {α : Sort u_1} {f : α → α} (h : Involutive f) : Involutive ⇑(toPerm f h)

theorem Function.Involutive.symm_eq_self_of_involutive {α : Sort u_1} (f : Equiv.Perm α) (h : Involutive ⇑f) : Equiv.symm f = f

theorem PLift.eq_up_iff_down_eq {α : Sort u_1} {x : PLift α} {y : α} : x = { down := y } ↔ x.down = y

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)

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 := ⋯ }

@[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)

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.

@[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.

@[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)).

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

@[simp]

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.

@[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)

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)).

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))

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

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

@[deprecated Equiv.piCongrLeft_sumInl (since := "2025-02-21")]

theorem Equiv.piCongrLeft_sum_inl {ι : 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

Alias of Equiv.piCongrLeft_sumInl.

@[deprecated Equiv.piCongrLeft_sumInr (since := "2025-02-21")]

theorem Equiv.piCongrLeft_sum_inr {ι : 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

Alias of Equiv.piCongrLeft_sumInr.

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₁)

@[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))

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))

@[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)

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

@[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))

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))

@[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)

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.

@[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, ⋯⟩

@[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, ⋯⟩

theorem Equiv.eq_conj {α : Sort u_9} {α' : Sort u_10} {β : Sort u_11} {β' : Sort u_12} (ε₁ : α ≃ α') (ε₂ : β' ≃ β) (f : α → β) (f' : α' → β') : ⇑ε₂.symm ∘ f ∘ ⇑ε₁.symm = f' ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁

theorem Equiv.semiconj_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁) : Function.Semiconj (⇑e) f (e.conj f)

theorem Equiv.semiconj₂_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) : Function.Semiconj₂ (⇑e) f ((e.arrowCongr e.conj) f)

instance Equiv.instAssociativeCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.Associative f] : Std.Associative ((e.arrowCongr (e.arrowCongr e)) f)

instance Equiv.instIdempotentOpCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [Std.IdempotentOp f] : Std.IdempotentOp ((e.arrowCongr (e.arrowCongr e)) f)

@[simp]

theorem Equiv.ulift_symm_down {α : Type v} (x : α) : (Equiv.ulift.symm x).down = x

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)

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)

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 := ⋯ }

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

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 := ⋯ }

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

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

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'

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

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