Equivalence between types #
In this file we continue the work on equivalences begun in Logic/Equiv/Defs.lean, defining
canonical isomorphisms between various types: e.g.,
Equiv.sumEquivSigmaBoolis the canonical equivalence between the sum of two typesα ⊕ βand the sigma-typeΣ b : Bool, b.casesOn α β;Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)shows that type product and type sum satisfy the distributive law up to a canonical equivalence;
operations on equivalences: e.g.,
Equiv.prodCongr ea eb : α₁ × β₁ ≃ α₂ × β₂: combine two equivalencesea : α₁ ≃ α₂andeb : β₁ ≃ β₂usingProd.map.
More definitions of this kind can be found in other files. E.g.,
Data/Equiv/TransferInstance.leandoes it for many algebraic type classes likeGroup,Module, etc.
Tags #
equivalence, congruence, bijective map
Type product is commutative up to an equivalence: α × β ≃ β × α. This is Prod.swap as an
equivalence.
Equations
- Equiv.prodComm α β = { toFun := Prod.swap, invFun := Prod.swap, left_inv := ⋯, right_inv := ⋯ }
@[simp]
@[simp]
theorem
Equiv.prodComm_apply
{α : Type u_1}
{β : Type u_2}
(x : α × β)
:
(Equiv.prodComm α β) x = x.swap
@[simp]
theorem
Equiv.prodComm_symm
(α : Type u_1)
(β : Type u_2)
:
(Equiv.prodComm α β).symm = Equiv.prodComm β α
@[simp]
theorem
Equiv.prodAssoc_apply
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
(p : (α × β) × γ)
:
(Equiv.prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)
@[simp]
theorem
Equiv.prodAssoc_symm_apply
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
(p : α × β × γ)
:
(Equiv.prodAssoc α β γ).symm p = ((p.1, p.2.1), p.2.2)
Type product is associative up to an equivalence.
@[simp]
theorem
Equiv.prodProdProdComm_symm
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
(δ : Type u_4)
:
(Equiv.prodProdProdComm α β γ δ).symm = Equiv.prodProdProdComm α γ β δ
@[simp]
theorem
Equiv.curry_apply
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
:
⇑(Equiv.curry α β γ) = Function.curry
@[simp]
theorem
Equiv.curry_symm_apply
(α : Type u_1)
(β : Type u_2)
(γ : Type u_3)
:
⇑(Equiv.curry α β γ).symm = Function.uncurry
γ-valued functions on α × β are equivalent to functions α → β → γ.
Equations
- Equiv.curry α β γ = { toFun := Function.curry, invFun := Function.uncurry, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.prodPUnit_symm_apply
(α : Type u_1)
(a : α)
:
(Equiv.prodPUnit α).symm a = (a, PUnit.unit)
@[simp]
theorem
Equiv.prodPUnit_apply
(α : Type u_1)
(p : α × PUnit.{u_2 + 1} )
:
(Equiv.prodPUnit α) p = p.1
PUnit is a right identity for type product up to an equivalence.
Equations
- Equiv.prodPUnit α = { toFun := fun (p : α × PUnit.{u_2 + 1} ) => p.1, invFun := fun (a : α) => (a, PUnit.unit), left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.punitProd_apply
(α : Type u_1)
:
∀ (a : PUnit.{u_2 + 1} × α), (Equiv.punitProd α) a = a.2
@[simp]
theorem
Equiv.punitProd_symm_apply
(α : Type u_1)
:
∀ (a : α), (Equiv.punitProd α).symm a = (PUnit.unit, a)
PUnit is a left identity for type product up to an equivalence.
Equations
@[simp]
theorem
Equiv.sigmaPUnit_apply
(α : Type u_1)
(p : (_ : α) × PUnit.{u_2 + 1} )
:
(Equiv.sigmaPUnit α) p = p.fst
@[simp]
theorem
Equiv.sigmaPUnit_symm_apply_fst
(α : Type u_1)
(a : α)
:
((Equiv.sigmaPUnit α).symm a).fst = a
@[simp]
theorem
Equiv.sigmaPUnit_symm_apply_snd
(α : Type u_1)
(a : α)
:
((Equiv.sigmaPUnit α).symm a).snd = PUnit.unit
PUnit is a right identity for dependent type product up to an equivalence.
Equations
- Equiv.sigmaPUnit α = { toFun := fun (p : (_ : α) × PUnit.{u_2 + 1} ) => p.fst, invFun := fun (a : α) => ⟨a, PUnit.unit⟩, left_inv := ⋯, right_inv := ⋯ }
Any Unique type is a right identity for type product up to equivalence.
Equations
- Equiv.prodUnique α β = ((Equiv.refl α).prodCongr (Equiv.equivPUnit β)).trans (Equiv.prodPUnit α)
@[simp]
theorem
Equiv.coe_prodUnique
{β : Type u_1}
{α : Type u_2}
[Unique β]
:
⇑(Equiv.prodUnique α β) = Prod.fst
theorem
Equiv.prodUnique_apply
{β : Type u_1}
{α : Type u_2}
[Unique β]
(x : α × β)
:
(Equiv.prodUnique α β) x = x.1
@[simp]
theorem
Equiv.prodUnique_symm_apply
{β : Type u_1}
{α : Type u_2}
[Unique β]
(x : α)
:
(Equiv.prodUnique α β).symm x = (x, default)
Any Unique type is a left identity for type product up to equivalence.
Equations
- Equiv.uniqueProd α β = ((Equiv.equivPUnit β).prodCongr (Equiv.refl α)).trans (Equiv.punitProd α)
@[simp]
theorem
Equiv.coe_uniqueProd
{β : Type u_1}
{α : Type u_2}
[Unique β]
:
⇑(Equiv.uniqueProd α β) = Prod.snd
theorem
Equiv.uniqueProd_apply
{β : Type u_1}
{α : Type u_2}
[Unique β]
(x : β × α)
:
(Equiv.uniqueProd α β) x = x.2
@[simp]
theorem
Equiv.uniqueProd_symm_apply
{β : Type u_1}
{α : Type u_2}
[Unique β]
(x : α)
:
(Equiv.uniqueProd α β).symm x = (default, x)
Any family of Unique types is a right identity for dependent type product up to
equivalence.
Equations
- Equiv.sigmaUnique α β = (Equiv.sigmaCongrRight fun (a : α) => Equiv.equivPUnit (β a)).trans (Equiv.sigmaPUnit α)
@[simp]
theorem
Equiv.coe_sigmaUnique
{α : Type u_2}
{β : α → Type u_1}
[(a : α) → Unique (β a)]
:
⇑(Equiv.sigmaUnique α β) = Sigma.fst
theorem
Equiv.sigmaUnique_apply
{α : Type u_2}
{β : α → Type u_1}
[(a : α) → Unique (β a)]
(x : (a : α) × β a)
:
(Equiv.sigmaUnique α β) x = x.fst
@[simp]
theorem
Equiv.sigmaUnique_symm_apply
{α : Type u_2}
{β : α → Type u_1}
[(a : α) → Unique (β a)]
(x : α)
:
(Equiv.sigmaUnique α β).symm x = ⟨x, default⟩
Empty type is a right absorbing element for type product up to an equivalence.
Equations
- Equiv.prodEmpty α = Equiv.equivEmpty (α × Empty)
Empty type is a left absorbing element for type product up to an equivalence.
Equations
- Equiv.emptyProd α = Equiv.equivEmpty (Empty × α)
PEmpty type is a right absorbing element for type product up to an equivalence.
Equations
PEmpty type is a left absorbing element for type product up to an equivalence.
Equations
Equations
- Equiv.psumEquivSum α β = { toFun := fun (s : α ⊕' β) => PSum.casesOn s Sum.inl Sum.inr, invFun := Sum.elim PSum.inl PSum.inr, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.sumCongr_refl
{α : Type u_1}
{β : Type u_2}
:
(Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)
@[reducible, inline]
abbrev
Equiv.Perm.sumCongr
{α : Type u_1}
{β : Type u_2}
(ea : Equiv.Perm α)
(eb : Equiv.Perm β)
:
Equiv.Perm (α ⊕ β)
Combine a permutation of α and of β into a permutation of α ⊕ β.
Equations
- ea.sumCongr eb = Equiv.sumCongr ea eb
@[simp]
theorem
Equiv.Perm.sumCongr_apply
{α : Type u_1}
{β : Type u_2}
(ea : Equiv.Perm α)
(eb : Equiv.Perm β)
(x : α ⊕ β)
:
theorem
Equiv.Perm.sumCongr_trans
{α : Type u_1}
{β : Type u_2}
(e : Equiv.Perm α)
(f : Equiv.Perm β)
(g : Equiv.Perm α)
(h : Equiv.Perm β)
:
Equiv.trans (e.sumCongr f) (g.sumCongr h) = Equiv.Perm.sumCongr (Equiv.trans e g) (Equiv.trans f h)
theorem
Equiv.Perm.sumCongr_symm
{α : Type u_1}
{β : Type u_2}
(e : Equiv.Perm α)
(f : Equiv.Perm β)
:
Equiv.symm (e.sumCongr f) = Equiv.Perm.sumCongr (Equiv.symm e) (Equiv.symm f)
theorem
Equiv.Perm.sumCongr_refl
{α : Type u_1}
{β : Type u_2}
:
Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)
@[simp]
Sum of types is commutative up to an equivalence. This is Sum.swap as an equivalence.
Equations
- Equiv.sumComm α β = { toFun := Sum.swap, invFun := Sum.swap, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.sumComm_symm
(α : Type u_1)
(β : Type u_2)
:
(Equiv.sumComm α β).symm = Equiv.sumComm β α
@[simp]
theorem
Equiv.sumAssoc_apply_inl_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(a : α)
:
(Equiv.sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
@[simp]
theorem
Equiv.sumAssoc_apply_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(c : γ)
:
(Equiv.sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
@[simp]
theorem
Equiv.sumAssoc_symm_apply_inl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(a : α)
:
(Equiv.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
@[simp]
theorem
Equiv.sumAssoc_symm_apply_inr_inr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(c : γ)
:
(Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
@[simp]
theorem
Equiv.sumEmpty_symm_apply
(α : Type u_1)
(β : Type u_2)
[IsEmpty β]
(val : α)
:
(Equiv.sumEmpty α β).symm val = Sum.inl val
Sum with IsEmpty is equivalent to the original type.
Equations
- Equiv.sumEmpty α β = { toFun := Sum.elim id fun (a : β) => isEmptyElim a, invFun := Sum.inl, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.sumEmpty_apply_inl
{β : Type u_1}
{α : Type u_2}
[IsEmpty β]
(a : α)
:
(Equiv.sumEmpty α β) (Sum.inl a) = a
@[simp]
theorem
Equiv.emptySum_symm_apply
(α : Type u_1)
(β : Type u_2)
[IsEmpty α]
:
∀ (a : β), (Equiv.emptySum α β).symm a = Sum.inr a
The sum of IsEmpty with any type is equivalent to that type.
Equations
- Equiv.emptySum α β = (Equiv.sumComm α β).trans (Equiv.sumEmpty β α)
@[simp]
theorem
Equiv.emptySum_apply_inr
{α : Type u_1}
{β : Type u_2}
[IsEmpty α]
(b : β)
:
(Equiv.emptySum α β) (Sum.inr b) = b
@[simp]
theorem
Equiv.optionEquivSumPUnit_none
{α : Type u_1}
:
(Equiv.optionEquivSumPUnit α) none = Sum.inr PUnit.unit
@[simp]
theorem
Equiv.optionEquivSumPUnit_some
{α : Type u_1}
(a : α)
:
(Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a
@[simp]
theorem
Equiv.optionEquivSumPUnit_coe
{α : Type u_1}
(a : α)
:
(Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a
@[simp]
theorem
Equiv.optionEquivSumPUnit_symm_inl
{α : Type u_1}
(a : α)
:
(Equiv.optionEquivSumPUnit α).symm (Sum.inl a) = some a
@[simp]
theorem
Equiv.optionEquivSumPUnit_symm_inr
{α : Type u_1}
(a : PUnit.{u_2 + 1} )
:
(Equiv.optionEquivSumPUnit α).symm (Sum.inr a) = none
@[simp]
theorem
Equiv.optionIsSomeEquiv_apply
(α : Type u_1)
(o : { x : Option α // x.isSome = true })
:
(Equiv.optionIsSomeEquiv α) o = (↑o).get ⋯
@[simp]
theorem
Equiv.optionIsSomeEquiv_symm_apply_coe
(α : Type u_1)
(x : α)
:
↑((Equiv.optionIsSomeEquiv α).symm x) = some x
The set of x : Option α such that isSome x is equivalent to α.
@[simp]
theorem
Equiv.piOptionEquivProd_symm_apply
{α : Type u_2}
{β : Option α → Type u_1}
(x : β none × ((a : α) → β (some a)))
(a : Option α)
:
Equiv.piOptionEquivProd.symm x a = Option.casesOn a x.1 x.2
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.
α ⊕ β is equivalent to a Sigma-type over Bool. Note that this definition assumes α and
β to be types from the same universe, so it cannot be used directly to transfer theorems about
sigma types to theorems about sum types. In many cases one can use ULift to work around this
difficulty.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.sigmaFiberEquiv_symm_apply_fst
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
:
((Equiv.sigmaFiberEquiv f).symm x).fst = f x
@[simp]
theorem
Equiv.sigmaFiberEquiv_symm_apply_snd_coe
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : α)
:
↑((Equiv.sigmaFiberEquiv f).symm x).snd = x
@[simp]
theorem
Equiv.sigmaFiberEquiv_apply
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(x : (y : β) × { x : α // f x = y })
:
(Equiv.sigmaFiberEquiv f) x = ↑x.snd
sigmaFiberEquiv f for f : α → β is the natural equivalence between
the type of all fibres of f and the total space α.
Equations
- Equiv.sigmaFiberEquiv f = { toFun := fun (x : (y : β) × { x : α // f x = y }) => ↑x.snd, invFun := fun (x : α) => ⟨f x, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }
Inhabited types are equivalent to Option β for some β by identifying default with none.
Equations
- One or more equations did not get rendered due to their size.
For any predicate p on α,
the sum of the two subtypes {a // p a} and its complement {a // ¬ p a}
is naturally equivalent to α.
See subtypeOrEquiv for sum types over subtypes {x // p x} and {x // q x}
that are not necessarily IsCompl p q.
Equations
- Equiv.sumCompl p = { toFun := Sum.elim Subtype.val Subtype.val, invFun := fun (a : α) => if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.sumCompl_apply_inl
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(x : { a : α // p a })
:
(Equiv.sumCompl p) (Sum.inl x) = ↑x
@[simp]
theorem
Equiv.sumCompl_apply_inr
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(x : { a : α // ¬p a })
:
(Equiv.sumCompl p) (Sum.inr x) = ↑x
@[simp]
theorem
Equiv.sumCompl_apply_symm_of_pos
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(a : α)
(h : p a)
:
(Equiv.sumCompl p).symm a = Sum.inl ⟨a, h⟩
@[simp]
theorem
Equiv.sumCompl_apply_symm_of_neg
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(a : α)
(h : ¬p a)
:
(Equiv.sumCompl p).symm a = Sum.inr ⟨a, h⟩
def
Equiv.subtypeCongr
{α : Type u_1}
{p : α → Prop}
{q : α → Prop}
[DecidablePred p]
[DecidablePred q]
(e : { x : α // p x } ≃ { x : α // q x })
(f : { x : α // ¬p x } ≃ { x : α // ¬q x })
:
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_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.Perm { a : ε // ¬p a })
:
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_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.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_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.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_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.Perm { a : ε // ¬p a })
(a : { a : ε // p a })
:
(ep.subtypeCongr en) ↑a = ↑(ep a)
@[simp]
theorem
Equiv.Perm.subtypeCongr.right_apply
{ε : Type u_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.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_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.Perm { a : ε // ¬p a })
(a : { a : ε // ¬p a })
:
(ep.subtypeCongr en) ↑a = ↑(en a)
@[simp]
theorem
Equiv.Perm.subtypeCongr.refl
{ε : Type u_1}
{p : ε → Prop}
[DecidablePred p]
:
Equiv.Perm.subtypeCongr (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) = Equiv.refl ε
@[simp]
theorem
Equiv.Perm.subtypeCongr.symm
{ε : Type u_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(en : Equiv.Perm { a : ε // ¬p a })
:
Equiv.symm (ep.subtypeCongr en) = Equiv.Perm.subtypeCongr (Equiv.symm ep) (Equiv.symm en)
@[simp]
theorem
Equiv.Perm.subtypeCongr.trans
{ε : Type u_1}
{p : ε → Prop}
[DecidablePred p]
(ep : Equiv.Perm { a : ε // p a })
(ep' : Equiv.Perm { a : ε // p a })
(en : Equiv.Perm { a : ε // ¬p a })
(en' : Equiv.Perm { a : ε // ¬p a })
:
Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = Equiv.Perm.subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')
@[simp]
theorem
Equiv.subtypePreimage_symm_apply_coe
{α : Sort u_1}
{β : Sort u_2}
(p : α → Prop)
[DecidablePred p]
(x₀ : { a : α // p a } → β)
(x : { a : α // ¬p a } → β)
(a : α)
:
↑((Equiv.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_2}
(p : α → Prop)
[DecidablePred p]
(x₀ : { a : α // p a } → β)
(x : { x : α → β // x ∘ Subtype.val = x₀ })
(a : { a : α // ¬p a })
:
(Equiv.subtypePreimage p x₀) x a = ↑x ↑a
def
Equiv.subtypePreimage
{α : Sort u_1}
{β : Sort u_2}
(p : α → Prop)
[DecidablePred p]
(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.
theorem
Equiv.subtypePreimage_symm_apply_coe_pos
{α : Sort u_1}
{β : Sort u_2}
(p : α → Prop)
[DecidablePred p]
(x₀ : { a : α // p a } → β)
(x : { a : α // ¬p a } → β)
(a : α)
(h : p a)
:
↑((Equiv.subtypePreimage p x₀).symm x) a = x₀ ⟨a, h⟩
theorem
Equiv.subtypePreimage_symm_apply_coe_neg
{α : Sort u_1}
{β : Sort u_2}
(p : α → Prop)
[DecidablePred p]
(x₀ : { a : α // p a } → β)
(x : { a : α // ¬p a } → β)
(a : α)
(h : ¬p a)
:
↑((Equiv.subtypePreimage p x₀).symm x) a = x ⟨a, h⟩
def
Equiv.piCongrRight
{α : Sort u_3}
{β₁ : α → Sort u_1}
{β₂ : α → Sort u_2}
(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 := fun (H : (a : α) → β₁ a) (a : α) => (F a) (H a), invFun := fun (H : (a : α) → β₂ a) (a : α) => (F a).symm (H a), left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.piComm_apply
{α : Sort u_2}
{β : Sort u_3}
(φ : α → β → Sort u_1)
(f : (x : α) → (y : β) → φ x y)
(y : β)
(x : α)
:
(Equiv.piComm φ) f y x = Function.swap f y x
def
Equiv.piComm
{α : Sort u_2}
{β : Sort u_3}
(φ : α → β → Sort u_1)
:
((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_symm
{α : Sort u_2}
{β : Sort u_3}
{φ : α → β → Sort u_1}
:
(Equiv.piComm φ).symm = Equiv.piComm (Function.swap φ)
def
Equiv.piCurry
{α : Type u_3}
{β : α → Type u_1}
(γ : (a : α) → β a → Type u_2)
:
((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_3}
{β : α → Type u_1}
(γ : (a : α) → β a → Type u_2)
(f : (x : (i : α) × β i) → γ x.fst x.snd)
:
(Equiv.piCurry γ) f = Sigma.curry f
@[simp]
theorem
Equiv.piCurry_symm_apply
{α : Type u_3}
{β : α → Type u_1}
(γ : (a : α) → β a → Type u_2)
(f : (a : α) → (b : β a) → γ a b)
:
(Equiv.piCurry γ).symm f = Sigma.uncurry f
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence
between β₁ × α₁ and β₂ × α₁.
Equations
- Equiv.prodCongrLeft e = { toFun := fun (ab : β₁ × α₁) => ((e ab.2) ab.1, ab.2), invFun := fun (ab : β₂ × α₁) => ((e ab.2).symm ab.1, ab.2), left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.prodCongrLeft_apply
{α₁ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_1}
(e : α₁ → β₁ ≃ β₂)
(b : β₁)
(a : α₁)
:
(Equiv.prodCongrLeft e) (b, a) = ((e a) b, a)
theorem
Equiv.prodCongr_refl_right
{α₁ : Type u_3}
{β₁ : Type u_1}
{β₂ : Type u_2}
(e : β₁ ≃ β₂)
:
e.prodCongr (Equiv.refl α₁) = Equiv.prodCongrLeft fun (x : α₁) => e
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence
between α₁ × β₁ and α₁ × β₂.
Equations
- Equiv.prodCongrRight e = { toFun := fun (ab : α₁ × β₁) => (ab.1, (e ab.1) ab.2), invFun := fun (ab : α₁ × β₂) => (ab.1, (e ab.1).symm ab.2), left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Equiv.prodCongrRight_apply
{α₁ : Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_1}
(e : α₁ → β₁ ≃ β₂)
(a : α₁)
(b : β₁)
:
(Equiv.prodCongrRight e) (a, b) = (a, (e a) b)
theorem
Equiv.prodCongr_refl_left
{α₁ : Type u_3}
{β₁ : Type u_1}
{β₂ : Type u_2}
(e : β₁ ≃ β₂)
:
(Equiv.refl α₁).prodCongr e = Equiv.prodCongrRight fun (x : α₁) => e
@[simp]
theorem
Equiv.prodCongrLeft_trans_prodComm
{α₁ : Type u_3}
{β₁ : Type u_2}
{β₂ : Type u_1}
(e : α₁ → β₁ ≃ β₂)
:
(Equiv.prodCongrLeft e).trans (Equiv.prodComm β₂ α₁) = (Equiv.prodComm β₁ α₁).trans (Equiv.prodCongrRight e)
@[simp]
theorem
Equiv.prodCongrRight_trans_prodComm
{α₁ : Type u_3}
{β₁ : Type u_2}
{β₂ : Type u_1}
(e : α₁ → β₁ ≃ β₂)
:
(Equiv.prodCongrRight e).trans (Equiv.prodComm α₁ β₂) = (Equiv.prodComm α₁ β₁).trans (Equiv.prodCongrLeft e)
theorem
Equiv.sigmaCongrRight_sigmaEquivProd
{α₁ : Type u_1}
{β₁ : Type u_3}
{β₂ : Type u_2}
(e : α₁ → β₁ ≃ β₂)
:
(Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂) = (Equiv.sigmaEquivProd α₁ β₁).trans (Equiv.prodCongrRight e)
theorem
Equiv.sigmaEquivProd_sigmaCongrRight
{α₁ : Type u_2}
{β₁ : Type u_1}
{β₂ : Type u_3}
(e : α₁ → β₁ ≃ β₂)
:
(Equiv.sigmaEquivProd α₁ β₁).symm.trans (Equiv.sigmaCongrRight e) = (Equiv.prodCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂).symm
@[simp]
theorem
Equiv.ofFiberEquiv_apply
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
{f : α → γ}
{g : β → γ}
(e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c })
:
∀ (a : α), (Equiv.ofFiberEquiv e) a = ↑((e (f a)) ((Equiv.sigmaFiberEquiv f).symm a).snd)
@[simp]
theorem
Equiv.ofFiberEquiv_symm_apply
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
{f : α → γ}
{g : β → γ}
(e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c })
:
∀ (a : β), (Equiv.ofFiberEquiv e).symm a = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a)).snd
def
Equiv.ofFiberEquiv
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
{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))
theorem
Equiv.ofFiberEquiv_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → γ}
{g : β → γ}
(e : (c : γ) → { a : α // f a = c } ≃ { b : β // g b = c })
(a : α)
:
g ((Equiv.ofFiberEquiv e) a) = f a
def
Equiv.prodShear
{α₁ : Type u_1}
{β₁ : Type u_2}
{β₂ : Type u_3}
{α₂ : Type u_4}
(e₁ : α₁ ≃ α₂)
(e₂ : α₁ → β₁ ≃ β₂)
:
A variation on Equiv.prodCongr where the equivalence in the second component can depend
on the first component. A typical example is a shear mapping, explaining the name of this
declaration.
def
Equiv.Perm.prodExtendRight
{α₁ : Type u_1}
{β₁ : Type u_2}
[DecidableEq α₁]
(a : α₁)
(e : Equiv.Perm β₁)
:
Equiv.Perm (α₁ × β₁)
prodExtendRight a e extends e : Perm β to Perm (α × β) by sending (a, b) to
(a, e b) and keeping the other (a', b) fixed.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.Perm.prodExtendRight_apply_eq
{α₁ : Type u_2}
{β₁ : Type u_1}
[DecidableEq α₁]
(a : α₁)
(e : Equiv.Perm β₁)
(b : β₁)
:
(Equiv.Perm.prodExtendRight a e) (a, b) = (a, e b)
theorem
Equiv.Perm.prodExtendRight_apply_ne
{α₁ : Type u_1}
{β₁ : Type u_2}
[DecidableEq α₁]
(e : Equiv.Perm β₁)
{a : α₁}
{a' : α₁}
(h : a' ≠ a)
(b : β₁)
:
(Equiv.Perm.prodExtendRight a e) (a', b) = (a', b)
theorem
Equiv.Perm.eq_of_prodExtendRight_ne
{α₁ : Type u_2}
{β₁ : Type u_1}
[DecidableEq α₁]
{e : Equiv.Perm β₁}
{a : α₁}
{a' : α₁}
{b : β₁}
(h : (Equiv.Perm.prodExtendRight a e) (a', b) ≠ (a', b))
:
a' = a
@[simp]
theorem
Equiv.Perm.fst_prodExtendRight
{α₁ : Type u_1}
{β₁ : Type u_2}
[DecidableEq α₁]
(a : α₁)
(e : Equiv.Perm β₁)
(ab : α₁ × β₁)
:
((Equiv.Perm.prodExtendRight a e) ab).1 = ab.1
The type of dependent functions on a sum type ι ⊕ ι' is equivalent to the type of pairs of
functions on ι and on ι'. This is a dependent version of Equiv.sumArrowEquivProdArrow.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.prodPiEquivSumPi_symm_apply
{ι : Type u_1}
{ι' : Type u_2}
(π : ι → Type u)
(π' : ι' → Type u)
:
∀ (a : (i : ι ⊕ ι') → Sum.elim π π' i),
(Equiv.prodPiEquivSumPi π π').symm a = (Equiv.sumPiEquivProdPi (Sum.elim π π')) a
@[simp]
theorem
Equiv.prodPiEquivSumPi_apply
{ι : Type u_1}
{ι' : Type u_2}
(π : ι → Type u)
(π' : ι' → Type u)
:
∀ (a : ((i : ι) → Sum.elim π π' (Sum.inl i)) × ((i' : ι') → Sum.elim π π' (Sum.inr i'))) (i : ι ⊕ ι'),
(Equiv.prodPiEquivSumPi π π') a i = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm a i
The equivalence between a product of two dependent functions types and a single dependent
function type. Basically a symmetric version of Equiv.sumPiEquivProdPi.
Equations
- Equiv.prodPiEquivSumPi π π' = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm
The type of functions on a sum type α ⊕ β is equivalent to the type of pairs of functions
on α and on β.
@[simp]
theorem
Equiv.sumArrowEquivProdArrow_apply_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α ⊕ β → γ)
(a : α)
:
((Equiv.sumArrowEquivProdArrow α β γ) f).1 a = f (Sum.inl a)
@[simp]
theorem
Equiv.sumArrowEquivProdArrow_apply_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α ⊕ β → γ)
(b : β)
:
((Equiv.sumArrowEquivProdArrow α β γ) f).2 b = f (Sum.inr b)
@[simp]
theorem
Equiv.sumArrowEquivProdArrow_symm_apply_inl
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
(f : α → γ)
(g : β → γ)
(a : α)
:
(Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inl a) = f a
@[simp]
theorem
Equiv.sumArrowEquivProdArrow_symm_apply_inr
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
(f : α → γ)
(g : β → γ)
(b : β)
:
(Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inr b) = g b
@[simp]
theorem
Equiv.sumProdDistrib_apply_left
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
(a : α)
(c : γ)
:
(Equiv.sumProdDistrib α β γ) (Sum.inl a, c) = Sum.inl (a, c)
@[simp]
theorem
Equiv.sumProdDistrib_apply_right
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
(b : β)
(c : γ)
:
(Equiv.sumProdDistrib α β γ) (Sum.inr b, c) = Sum.inr (b, c)
@[simp]
theorem
Equiv.sumProdDistrib_symm_apply_left
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
(a : α × γ)
:
(Equiv.sumProdDistrib α β γ).symm (Sum.inl a) = (Sum.inl a.1, a.2)
@[simp]
theorem
Equiv.sumProdDistrib_symm_apply_right
{β : Type u_1}
{γ : Type u_2}
{α : Type u_3}
(b : β × γ)
:
(Equiv.sumProdDistrib α β γ).symm (Sum.inr b) = (Sum.inr b.1, b.2)
Type product is left distributive with respect to type sum up to an equivalence.
Equations
- Equiv.prodSumDistrib α β γ = Trans.trans (Trans.trans (Equiv.prodComm α (β ⊕ γ)) (Equiv.sumProdDistrib β γ α)) ((Equiv.prodComm β α).sumCongr (Equiv.prodComm γ α))
@[simp]
theorem
Equiv.prodSumDistrib_apply_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(a : α)
(b : β)
:
(Equiv.prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)
@[simp]
theorem
Equiv.prodSumDistrib_apply_right
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
(a : α)
(c : γ)
:
(Equiv.prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)
@[simp]
theorem
Equiv.prodSumDistrib_symm_apply_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(a : α × β)
:
(Equiv.prodSumDistrib α β γ).symm (Sum.inl a) = (a.1, Sum.inl a.2)
@[simp]
theorem
Equiv.prodSumDistrib_symm_apply_right
{α : Type u_1}
{γ : Type u_2}
{β : Type u_3}
(a : α × γ)
:
(Equiv.prodSumDistrib α β γ).symm (Sum.inr a) = (a.1, Sum.inr a.2)
The product of an indexed sum of types (formally, a Sigma-type Σ i, α i) by a type β is
equivalent to the sum of products Σ i, (α i × β).
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.boolProdEquivSum_apply
(α : Type u_1)
(p : Bool × α)
:
(Equiv.boolProdEquivSum α) p = Bool.casesOn p.1 (Sum.inl p.2) (Sum.inr p.2)
The product Bool × α is equivalent to α ⊕ α.
@[simp]
theorem
Equiv.boolArrowEquivProd_symm_apply
(α : Type u_1)
(p : α × α)
(b : Bool)
:
(Equiv.boolArrowEquivProd α).symm p b = Bool.casesOn b p.1 p.2
@[simp]
theorem
Equiv.boolArrowEquivProd_apply
(α : Type u_1)
(f : Bool → α)
:
(Equiv.boolArrowEquivProd α) f = (f false, f true)
The function type Bool → α is equivalent to α × α.
Equations
- Equiv.boolArrowEquivProd α = { toFun := fun (f : Bool → α) => (f false, f true), invFun := fun (p : α × α) (b : Bool) => Bool.casesOn b p.1 p.2, left_inv := ⋯, right_inv := ⋯ }
The set of natural numbers is equivalent to ℕ ⊕ PUnit.
Equations
- One or more equations did not get rendered due to their size.
ℕ ⊕ PUnit is equivalent to ℕ.
Equations
def
Equiv.subtypeEquiv
{α : Sort u_1}
{β : Sort u_2}
{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 := ⋯ }
theorem
Equiv.coe_subtypeEquiv_eq_map
{X : Type u_1}
{Y : Type u_2}
{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 : optParam (∀ (a : α), p a ↔ p ((Equiv.refl α) a)) ⋯)
:
(Equiv.refl α).subtypeEquiv h = Equiv.refl { a : α // p a }
@[simp]
theorem
Equiv.subtypeEquivRight_apply_coe
{α : Sort u_1}
{p : α → Prop}
{q : α → Prop}
(e : ∀ (x : α), p x ↔ q x)
(a : { a : α // p a })
:
↑((Equiv.subtypeEquivRight e) a) = ↑a
@[simp]
theorem
Equiv.subtypeEquivRight_symm_apply_coe
{α : Sort u_1}
{p : α → Prop}
{q : α → Prop}
(e : ∀ (x : α), p x ↔ q x)
(b : { b : α // q b })
:
↑((Equiv.subtypeEquivRight e).symm b) = ↑b
def
Equiv.subtypeEquivRight
{α : Sort u_1}
{p : α → Prop}
{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
theorem
Equiv.subtypeEquivRight_apply
{α : Sort u_1}
{p : α → Prop}
{q : α → Prop}
(e : ∀ (x : α), p x ↔ q x)
(z : { x : α // p x })
:
(Equiv.subtypeEquivRight e) z = ⟨↑z, ⋯⟩
theorem
Equiv.subtypeEquivRight_symm_apply
{α : Sort u_1}
{p : α → Prop}
{q : α → Prop}
(e : ∀ (x : α), p x ↔ q x)
(z : { x : α // q x })
:
(Equiv.subtypeEquivRight e).symm z = ⟨↑z, ⋯⟩
def
Equiv.subtypeEquivOfSubtype'
{α : Sort u_1}
{β : Sort u_2}
{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
If two predicates are equal, then the corresponding subtypes are equivalent.
Equations
- Equiv.subtypeEquivProp h = (Equiv.refl α).subtypeEquiv ⋯
@[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⟩ })
:
↑↑((Equiv.subtypeSubtypeEquivSubtypeExists p q).symm a) = ↑a
@[simp]
theorem
Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe
{α : Sort u_1}
(p : α → Prop)
(q : Subtype p → Prop)
(a : Subtype q)
:
↑((Equiv.subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a
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.subtypeSubtypeEquivSubtypeInter_apply_coe
{α : Type u}
(p : α → Prop)
(q : α → Prop)
:
∀ (a : { x : Subtype p // q ↑x }), ↑((Equiv.subtypeSubtypeEquivSubtypeInter p q) a) = ↑↑a
@[simp]
theorem
Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe
{α : Type u}
(p : α → Prop)
(q : α → Prop)
:
∀ (a : { x : α // p x ∧ q x }), ↑↑((Equiv.subtypeSubtypeEquivSubtypeInter p q).symm a) = ↑a
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.subtypeSubtypeEquivSubtype_symm_apply_coe_coe
{α : Type u_1}
{p : α → Prop}
{q : α → Prop}
(h : ∀ {x : α}, q x → p x)
:
∀ (a : Subtype q), ↑↑((Equiv.subtypeSubtypeEquivSubtype h).symm a) = ↑a
@[simp]
theorem
Equiv.subtypeSubtypeEquivSubtype_apply_coe
{α : Type u_1}
{p : α → Prop}
{q : α → Prop}
(h : ∀ {x : α}, q x → p x)
:
∀ (a : { x : Subtype p // q ↑x }), ↑((Equiv.subtypeSubtypeEquivSubtype h) a) = ↑↑a
def
Equiv.subtypeSubtypeEquivSubtype
{α : Type u_1}
{p : α → Prop}
{q : α → Prop}
(h : ∀ {x : α}, q x → p x)
:
If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.
Equations
@[simp]
theorem
Equiv.subtypeUnivEquiv_symm_apply
{α : Type u_1}
{p : α → Prop}
(h : ∀ (x : α), p x)
(x : α)
:
(Equiv.subtypeUnivEquiv h).symm x = ⟨x, ⋯⟩
@[simp]
theorem
Equiv.subtypeUnivEquiv_apply
{α : Type u_1}
{p : α → Prop}
(h : ∀ (x : α), p x)
(x : Subtype p)
:
(Equiv.subtypeUnivEquiv h) x = ↑x
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 := ⋯ }
def
Equiv.sigmaSubtypeEquivOfSubset
{α : Type u_1}
(p : α → Type v)
(q : α → Prop)
(h : ∀ (x : α), p x → q 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_1}
{β : Type u_2}
(f : α → β)
(p : β → Prop)
(h : ∀ (x : α), p (f x))
:
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_1}
{β : Type u_2}
(f : α → β)
{p : α → Prop}
{q : β → Prop}
(h : ∀ (x : α), p x ↔ q (f x))
:
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.
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'
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.
A subtype of a product defined by componentwise conditions is equivalent to a product of subtypes.
Equations
- One or more equations did not get rendered due to their size.
A subtype of a Prod that depends only on the first component is equivalent to the
corresponding subtype of the first type times the second type.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.piEquivPiSubtypeProd_symm_apply
{α : Type u_1}
(p : α → Prop)
(β : α → Type u_2)
[DecidablePred p]
(f : ((i : { x : α // p x }) → β ↑i) × ((i : { x : α // ¬p x }) → β ↑i))
(x : α)
:
(Equiv.piEquivPiSubtypeProd p β).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
@[simp]
theorem
Equiv.piEquivPiSubtypeProd_apply
{α : Type u_1}
(p : α → Prop)
(β : α → Type u_2)
[DecidablePred p]
(f : (i : α) → β i)
:
(Equiv.piEquivPiSubtypeProd p β) f = (fun (x : { x : α // p x }) => f ↑x, fun (x : { x : α // ¬p x }) => f ↑x)
The type ∀ (i : α), β i can be split as a product by separating the indices in α
depending on whether they satisfy a predicate p or not.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.piSplitAt_apply
{α : Type u_1}
[DecidableEq α]
(i : α)
(β : α → Type u_2)
(f : (j : α) → β j)
:
(Equiv.piSplitAt i β) f = (f i, fun (j : { j : α // j ≠ i }) => f ↑j)
@[simp]
theorem
Equiv.piSplitAt_symm_apply
{α : Type u_1}
[DecidableEq α]
(i : α)
(β : α → Type u_2)
(f : β i × ((j : { j : α // j ≠ i }) → β ↑j))
(j : α)
:
(Equiv.piSplitAt i β).symm f j = if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩
A product of types can be split as the binary product of one of the types and the product of all the remaining types.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Equiv.funSplitAt_apply
{α : Type u_1}
[DecidableEq α]
(i : α)
(β : Type u_2)
(f : (j : α) → (fun (a : α) => β) j)
:
(Equiv.funSplitAt i β) f = (f i, fun (j : { j : α // ¬j = i }) => f ↑j)
@[simp]
theorem
Equiv.funSplitAt_symm_apply
{α : Type u_1}
[DecidableEq α]
(i : α)
(β : Type u_2)
(f : (fun (a : α) => β) i × ((j : { j : α // j ≠ i }) → (fun (a : α) => β) ↑j))
(j : α)
:
(Equiv.funSplitAt i β).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩
A product of copies of a type can be split as the binary product of one copy and the product of all the remaining copies.
Equations
- Equiv.funSplitAt i β = Equiv.piSplitAt i fun (a : α) => β
def
Equiv.subtypeEquivCodomain
{X : Sort u_1}
[DecidableEq X]
{x : X}
{Y : Sort u_2}
(f : { x' : X // x' ≠ x } → 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_2}
[DecidableEq X]
{x : X}
{Y : Sort u_1}
(f : { x' : X // x' ≠ x } → Y)
:
⇑(Equiv.subtypeEquivCodomain f) = fun (g : { g : X → Y // g ∘ Subtype.val = f }) => ↑g x
@[simp]
theorem
Equiv.subtypeEquivCodomain_apply
{X : Sort u_2}
[DecidableEq X]
{x : X}
{Y : Sort u_1}
(f : { x' : X // x' ≠ x } → Y)
(g : { g : X → Y // g ∘ Subtype.val = f })
:
(Equiv.subtypeEquivCodomain f) g = ↑g x
theorem
Equiv.coe_subtypeEquivCodomain_symm
{X : Sort u_2}
[DecidableEq X]
{x : X}
{Y : Sort u_1}
(f : { x' : X // x' ≠ x } → Y)
:
⇑(Equiv.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_2}
[DecidableEq X]
{x : X}
{Y : Sort u_1}
(f : { x' : X // x' ≠ x } → Y)
(y : Y)
(x' : X)
:
↑((Equiv.subtypeEquivCodomain f).symm y) x' = if h : x' ≠ x then f ⟨x', h⟩ else y
theorem
Equiv.subtypeEquivCodomain_symm_apply_eq
{X : Sort u_2}
[DecidableEq X]
{x : X}
{Y : Sort u_1}
(f : { x' : X // x' ≠ x } → Y)
(y : Y)
:
↑((Equiv.subtypeEquivCodomain f).symm y) x = y
theorem
Equiv.subtypeEquivCodomain_symm_apply_ne
{X : Sort u_2}
[DecidableEq X]
{x : X}
{Y : Sort u_1}
(f : { x' : X // x' ≠ x } → Y)
(y : Y)
(x' : X)
(h : x' ≠ x)
:
↑((Equiv.subtypeEquivCodomain f).symm y) x' = f ⟨x', h⟩
def
Equiv.Perm.extendDomain
{α' : Type u_1}
{β' : Type u_2}
(e : Equiv.Perm α')
{p : β' → Prop}
[DecidablePred p]
(f : α' ≃ Subtype p)
:
Equiv.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_1}
{β' : Type u_2}
(e : Equiv.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_1}
{β' : Type u_2}
(e : Equiv.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_1}
{β' : Type u_2}
(e : Equiv.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_1}
{β' : Type u_2}
{p : β' → Prop}
[DecidablePred p]
(f : α' ≃ Subtype p)
:
Equiv.Perm.extendDomain (Equiv.refl α') f = Equiv.refl β'
@[simp]
theorem
Equiv.Perm.extendDomain_symm
{α' : Type u_1}
{β' : Type u_2}
(e : Equiv.Perm α')
{p : β' → Prop}
[DecidablePred p]
(f : α' ≃ Subtype p)
:
Equiv.symm (e.extendDomain f) = Equiv.Perm.extendDomain (Equiv.symm e) f
theorem
Equiv.Perm.extendDomain_trans
{α' : Type u_1}
{β' : Type u_2}
{p : β' → Prop}
[DecidablePred p]
(f : α' ≃ Subtype p)
(e : Equiv.Perm α')
(e' : Equiv.Perm α')
:
Equiv.trans (e.extendDomain f) (e'.extendDomain f) = Equiv.Perm.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₁), Setoid.r x y ↔ Setoid.r ↑x ↑y)
:
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₁), Setoid.r x y ↔ ↑x ≈ ↑y)
(x : α)
(hx : p₂ ⟦x⟧)
:
(Equiv.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₁), Setoid.r x y ↔ ↑x ≈ ↑y)
(x : Subtype p₁)
:
(Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm ⟦x⟧ = ⟨⟦↑x⟧, ⋯⟩
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 : α)
:
Equiv.swapCore a a r = r
theorem
Equiv.swapCore_swapCore
{α : Sort u_1}
[DecidableEq α]
(r : α)
(a : α)
(b : α)
:
Equiv.swapCore a b (Equiv.swapCore a b r) = r
theorem
Equiv.swapCore_comm
{α : Sort u_1}
[DecidableEq α]
(r : α)
(a : α)
(b : α)
:
Equiv.swapCore a b r = Equiv.swapCore b a r
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_comm
{α : Sort u_1}
[DecidableEq α]
(a : α)
(b : α)
:
Equiv.swap a b = Equiv.swap b a
theorem
Equiv.swap_apply_def
{α : Sort u_1}
[DecidableEq α]
(a : α)
(b : α)
(x : α)
:
(Equiv.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 : α)
:
(Equiv.swap a b) a = b
@[simp]
theorem
Equiv.swap_apply_right
{α : Sort u_1}
[DecidableEq α]
(a : α)
(b : α)
:
(Equiv.swap a b) b = a
theorem
Equiv.swap_apply_of_ne_of_ne
{α : Sort u_1}
[DecidableEq α]
{a : α}
{b : α}
{x : α}
:
x ≠ a → x ≠ b → (Equiv.swap a b) x = x
theorem
Equiv.eq_or_eq_of_swap_apply_ne_self
{α : Sort u_1}
[DecidableEq α]
{a : α}
{b : α}
{x : α}
(h : (Equiv.swap a b) x ≠ x)
:
@[simp]
theorem
Equiv.swap_swap
{α : Sort u_1}
[DecidableEq α]
(a : α)
(b : α)
:
Equiv.trans (Equiv.swap a b) (Equiv.swap a b) = Equiv.refl α
@[simp]
theorem
Equiv.symm_swap
{α : Sort u_1}
[DecidableEq α]
(a : α)
(b : α)
:
Equiv.symm (Equiv.swap a b) = Equiv.swap a b
@[simp]
theorem
Equiv.swap_eq_refl_iff
{α : Sort u_1}
[DecidableEq α]
{x : α}
{y : α}
:
Equiv.swap x y = Equiv.refl α ↔ x = y
theorem
Equiv.swap_comp_apply
{α : Sort u_1}
[DecidableEq α]
{a : α}
{b : α}
{x : α}
(π : Equiv.Perm α)
:
(Equiv.trans π (Equiv.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 : α)
:
⇑(Equiv.swap i j) = Function.update (Function.update id j i) i j
theorem
Equiv.comp_swap_eq_update
{α : Sort u_2}
[DecidableEq α]
{β : Sort u_1}
(i : α)
(j : α)
(f : α → β)
:
f ∘ ⇑(Equiv.swap i j) = Function.update (Function.update f j (f i)) i (f j)
@[simp]
theorem
Equiv.symm_trans_swap_trans
{α : Sort u_2}
[DecidableEq α]
{β : Sort u_1}
[DecidableEq β]
(a : α)
(b : α)
(e : α ≃ β)
:
(e.symm.trans (Equiv.swap a b)).trans e = Equiv.swap (e a) (e b)
@[simp]
theorem
Equiv.trans_swap_trans_symm
{α : Sort u_2}
[DecidableEq α]
{β : Sort u_1}
[DecidableEq β]
(a : β)
(b : β)
(e : α ≃ β)
:
(e.trans (Equiv.swap a b)).trans e.symm = Equiv.swap (e.symm a) (e.symm b)
@[simp]
theorem
Equiv.swap_apply_self
{α : Sort u_1}
[DecidableEq α]
(i : α)
(j : α)
(a : α)
:
(Equiv.swap i j) ((Equiv.swap i j) a) = a
theorem
Equiv.apply_swap_eq_self
{α : Sort u_2}
[DecidableEq α]
{β : Sort u_1}
{v : α → β}
{i : α}
{j : α}
(hv : v i = v j)
(k : α)
:
v ((Equiv.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 : α}
:
(Equiv.swap x y) z = w ↔ z = (Equiv.swap x y) w
@[simp]
theorem
Equiv.Perm.sumCongr_swap_refl
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[DecidableEq β]
(i : α)
(j : α)
:
(Equiv.swap i j).sumCongr (Equiv.refl β) = Equiv.swap (Sum.inl i) (Sum.inl j)
@[simp]
theorem
Equiv.Perm.sumCongr_refl_swap
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[DecidableEq β]
(i : β)
(j : β)
:
Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)
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_2}
[DecidableEq α]
{β : Sort u_1}
(f : α ≃ β)
(a : α)
(b : β)
:
(f.setValue a b) a = b
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 : Function.Involutive f)
:
⇑(Function.Involutive.toPerm f h) = f
@[simp]
theorem
Function.Involutive.toPerm_involutive
{α : Sort u_1}
{f : α → α}
(h : Function.Involutive f)
:
theorem
Function.Injective.map_swap
{α : Sort u_1}
{β : Sort u_2}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
(hf : Function.Injective f)
(x : α)
(y : α)
(z : α)
:
f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
@[simp]
theorem
Equiv.piCongrLeft'_symm_apply
{α : Sort u_2}
{β : Sort u_3}
(P : α → Sort u_1)
(e : α ≃ β)
(f : (b : β) → P (e.symm b))
(x : α)
:
(Equiv.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'_apply
{α : Sort u_2}
{β : Sort u_3}
(P : α → Sort u_1)
(e : α ≃ β)
(f : (a : α) → P a)
(x : β)
:
(Equiv.piCongrLeft' P e) f x = f (e.symm x)
def
Equiv.piCongrLeft'
{α : Sort u_2}
{β : Sort u_3}
(P : α → Sort u_1)
(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'_symm
{α : Sort u_2}
{β : Sort u_3}
(P : Sort u_1)
(e : α ≃ β)
:
(Equiv.piCongrLeft' (fun (x : α) => P) e).symm = Equiv.piCongrLeft' (fun (a : β) => P) e.symm
This lemma is impractical to state in the dependent case.
theorem
Equiv.piCongrLeft'_symm_apply_apply
{α : Sort u_2}
{β : Sort u_3}
(P : α → Sort u_1)
(e : α ≃ β)
(g : (b : β) → P (e.symm b))
(b : β)
:
(Equiv.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_2}
(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_2}
(P : β → Sort w)
(e : α ≃ β)
(f : (a : α) → P (e a))
(b : β)
:
(Equiv.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_2}
(P : β → Sort w)
(e : α ≃ β)
(g : (b : β) → P b)
(a : α)
:
(Equiv.piCongrLeft P e).symm g a = g (e a)
theorem
Equiv.piCongrLeft_apply_apply
{β : Sort u_1}
{α : Sort u_2}
(P : β → Sort w)
(e : α ≃ β)
(f : (a : α) → P (e a))
(a : α)
:
(Equiv.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_2}
{α : Sort u_1}
{P : β → Sort v}
{e : α ≃ β}
(f : (a : α) → P (e a))
(b : β)
:
(Equiv.piCongrLeft P e) f b = cast ⋯ (f (e.symm b))
theorem
Equiv.piCongrLeft_sum_inl
{ι'' : Sort u_2}
{ι : Type u_3}
{ι' : Type u_4}
(π : ι'' → Type u_1)
(e : ι ⊕ ι' ≃ ι'')
(f : (i : ι) → π (e (Sum.inl i)))
(g : (i : ι') → π (e (Sum.inr i)))
(i : ι)
:
(Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun (x : ι ⊕ ι') => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i
theorem
Equiv.piCongrLeft_sum_inr
{ι'' : Sort u_2}
{ι : Type u_3}
{ι' : Type u_4}
(π : ι'' → Type u_1)
(e : ι ⊕ ι' ≃ ι'')
(f : (i : ι) → π (e (Sum.inl i)))
(g : (i : ι') → π (e (Sum.inr i)))
(j : ι')
:
(Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun (x : ι ⊕ ι') => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j
def
Equiv.piCongr
{α : Sort u_1}
{β : Sort u_2}
{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₁)
def
Equiv.piCongr'
{α : Sort u_1}
{β : Sort u_2}
{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
theorem
Equiv.semiconj_conj
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁)
:
Function.Semiconj (⇑e) f (e.conj f)
theorem
Equiv.semiconj₂_conj
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
:
Function.Semiconj₂ (⇑e) f ((e.arrowCongr e.conj) f)
instance
Equiv.instAssociativeCoeForallForallArrowCongr
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
[Std.Associative f]
:
Std.Associative ((e.arrowCongr (e.arrowCongr e)) f)
Equations
- ⋯ = ⋯
instance
Equiv.instIdempotentOpCoeForallForallArrowCongr
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
[Std.IdempotentOp f]
:
Std.IdempotentOp ((e.arrowCongr (e.arrowCongr e)) f)
Equations
- ⋯ = ⋯
instance
Equiv.instIsLeftCancelCoeForallForallArrowCongr
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
[IsLeftCancel α₁ f]
:
IsLeftCancel β₁ ((e.arrowCongr (e.arrowCongr e)) f)
Equations
- ⋯ = ⋯
instance
Equiv.instIsRightCancelCoeForallForallArrowCongr
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
[IsRightCancel α₁ f]
:
IsRightCancel β₁ ((e.arrowCongr (e.arrowCongr e)) f)
Equations
- ⋯ = ⋯
theorem
Function.Injective.swap_apply
{α : Sort u_1}
{β : Sort u_2}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
(hf : Function.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_2}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
(hf : Function.Injective f)
(x : α)
(y : α)
:
⇑(Equiv.swap (f x) (f y)) ∘ f = f ∘ ⇑(Equiv.swap x y)
If α is a subsingleton, then it is equivalent to α × α.
def
equivOfSubsingletonOfSubsingleton
{α : Sort u_1}
{β : Sort u_2}
[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_2}
A nonempty subsingleton type is (noncomputably) equivalent to PUnit.
Equations
- Equiv.punitOfNonemptyOfSubsingleton = equivOfSubsingletonOfSubsingleton (fun (x : α) => PUnit.unit) fun (x : PUnit.{u_2}) => h.some
If Unique β, then Unique α is equivalent to α ≃ β.
Equations
- uniqueEquivEquivUnique α β = equivOfSubsingletonOfSubsingleton (fun (x : Unique α) => Equiv.equivOfUnique α β) Equiv.unique
theorem
Function.update_comp_equiv
{α' : Sort u_1}
{α : Sort u_2}
{β : Sort u_3}
[DecidableEq α']
[DecidableEq α]
(f : α → β)
(g : α' ≃ α)
(a : α)
(v : β)
:
Function.update f a v ∘ ⇑g = Function.update (f ∘ ⇑g) (g.symm a) v
theorem
Function.update_apply_equiv_apply
{α' : Sort u_1}
{α : Sort u_2}
{β : Sort u_3}
[DecidableEq α']
[DecidableEq α]
(f : α → β)
(g : α' ≃ α)
(a : α)
(v : β)
(a' : α')
:
Function.update f a v (g a') = Function.update (f ∘ ⇑g) (g.symm a) v a'
theorem
Function.piCongrLeft'_update
{α : Sort u_2}
{β : Sort u_3}
[DecidableEq α]
[DecidableEq β]
(P : α → Sort u_1)
(e : α ≃ β)
(f : (a : α) → P a)
(b : β)
(x : P (e.symm b))
:
(Equiv.piCongrLeft' P e) (Function.update f (e.symm b) x) = Function.update ((Equiv.piCongrLeft' P e) f) b x
theorem
Function.piCongrLeft'_symm_update
{α : Sort u_2}
{β : Sort u_3}
[DecidableEq α]
[DecidableEq β]
(P : α → Sort u_1)
(e : α ≃ β)
(f : (b : β) → P (e.symm b))
(b : β)
(x : P (e.symm b))
:
(Equiv.piCongrLeft' P e).symm (Function.update f b x) = Function.update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x