Documentation

Mathlib.Logic.Equiv.Defs

Equivalence between types #

In this file we define two types:

Then we define

Many more such isomorphisms and operations are defined in Logic.Equiv.Basic.

Tags #

equivalence, congruence, bijective map

structure Equiv (α : Sort u_1) (β : Sort u_2) :
Sort (max(max1u_1)u_2)

α ≃ β≃ β is the type of functions from α → β→ β with a two-sided inverse.

Instances For
    def EquivLike.toEquiv {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] (f : F) :
    α β

    Turn an element of a type F satisfying EquivLike F α β into an actual Equiv. This is declared as the default coercion from F to α ≃ β≃ β.

    Equations
    • One or more equations did not get rendered due to their size.
    instance instCoeTCEquiv {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] :
    CoeTC F (α β)

    Any type satisfying EquivLike can be cast into Equiv via EquivLike.toEquiv.

    Equations
    • instCoeTCEquiv = { coe := EquivLike.toEquiv }
    def Equiv.Perm (α : Sort u_1) :
    Sort (max1u_1)

    Perm α is the type of bijections from α to itself.

    Equations
    instance Equiv.instEquivLikeEquiv {α : Sort u} {β : Sort v} :
    EquivLike (α β) α β
    Equations
    • One or more equations did not get rendered due to their size.
    instance Equiv.instFunLikeEquiv {α : Sort u} {β : Sort v} :
    FunLike (α β) α fun x => β

    Helper instance when inference gets stuck on following the normal chain EquivLike → EmbeddingLike → FunLike → CoeFun→ EmbeddingLike → FunLike → CoeFun→ FunLike → CoeFun→ CoeFun.

    Equations
    • Equiv.instFunLikeEquiv = EmbeddingLike.toFunLike
    @[simp]
    theorem Equiv.coe_fn_mk {α : Sort u} {β : Sort v} (f : αβ) (g : βα) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) :
    { toFun := f, invFun := g, left_inv := l, right_inv := r } = f
    theorem Equiv.coe_fn_injective {α : Sort u} {β : Sort v} :
    Function.Injective fun e => e

    The map (r ≃ s) → (r → s)≃ s) → (r → s)→ (r → s)→ s) is injective.

    theorem Equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ : α β} {e₂ : α β} :
    e₁ = e₂ e₁ = e₂
    theorem Equiv.ext {α : Sort u} {β : Sort v} {f : α β} {g : α β} (H : ∀ (x : α), f x = g x) :
    f = g
    theorem Equiv.congr_arg {α : Sort u} {β : Sort v} {f : α β} {x : α} {x' : α} :
    x = x'f x = f x'
    theorem Equiv.congr_fun {α : Sort u} {β : Sort v} {f : α β} {g : α β} (h : f = g) (x : α) :
    f x = g x
    theorem Equiv.ext_iff {α : Sort u} {β : Sort v} {f : α β} {g : α β} :
    f = g ∀ (x : α), f x = g x
    theorem Equiv.Perm.ext {α : Sort u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (H : ∀ (x : α), σ x = τ x) :
    σ = τ
    theorem Equiv.Perm.congr_arg {α : Sort u} {f : Equiv.Perm α} {x : α} {x' : α} :
    x = x'f x = f x'
    theorem Equiv.Perm.congr_fun {α : Sort u} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f = g) (x : α) :
    f x = g x
    theorem Equiv.Perm.ext_iff {α : Sort u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
    σ = τ ∀ (x : α), σ x = τ x
    def Equiv.refl (α : Sort u_1) :
    α α

    Any type is equivalent to itself.

    Equations
    • Equiv.refl α = { toFun := id, invFun := id, left_inv := (_ : ∀ (x : α), id (id x) = id (id x)), right_inv := (_ : ∀ (x : α), id (id x) = id (id x)) }
    instance Equiv.inhabited' {α : Sort u} :
    Inhabited (α α)
    Equations
    def Equiv.symm {α : Sort u} {β : Sort v} (e : α β) :
    β α

    Inverse of an equivalence e : α ≃ β≃ β.

    Equations
    def Equiv.Simps.symm_apply {α : Sort u} {β : Sort v} (e : α β) :
    βα

    See Note [custom simps projection]

    Equations
    theorem Equiv.left_inv' {α : Sort u} {β : Sort v} (e : α β) :
    theorem Equiv.right_inv' {α : Sort u} {β : Sort v} (e : α β) :
    def Equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
    α γ

    Composition of equivalences e₁ : α ≃ β≃ β and e₂ : β ≃ γ≃ γ.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.instTransSortSortSortEquivEquivEquiv_trans :
    ∀ {a : Sort u_2} {b : Sort u_1} {c : Sort u_3} (e₁ : a b) (e₂ : b c), Trans.trans e₁ e₂ = Equiv.trans e₁ e₂
    @[simp]
    theorem Equiv.toFun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
    e.toFun = e
    @[simp]
    theorem Equiv.toFun_as_coe_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
    Equiv.toFun e x = e x
    @[simp]
    theorem Equiv.invFun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
    e.invFun = ↑(Equiv.symm e)
    theorem Equiv.injective {α : Sort u} {β : Sort v} (e : α β) :
    theorem Equiv.surjective {α : Sort u} {β : Sort v} (e : α β) :
    theorem Equiv.bijective {α : Sort u} {β : Sort v} (e : α β) :
    theorem Equiv.subsingleton {α : Sort u} {β : Sort v} (e : α β) [inst : Subsingleton β] :
    theorem Equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α β) [inst : Subsingleton α] :
    theorem Equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α β) :
    instance Equiv.permUnique {α : Sort u} [inst : Subsingleton α] :
    Equations
    def Equiv.decidableEq {α : Sort u} {β : Sort v} (e : α β) [inst : DecidableEq β] :

    Transfer DecidableEq across an equivalence.

    Equations
    theorem Equiv.nonempty_congr {α : Sort u} {β : Sort v} (e : α β) :
    theorem Equiv.nonempty {α : Sort u} {β : Sort v} (e : α β) [inst : Nonempty β] :
    def Equiv.inhabited {α : Sort u} {β : Sort v} [inst : Inhabited β] (e : α β) :

    If α ≃ β≃ β and β is inhabited, then so is α.

    Equations
    def Equiv.unique {α : Sort u} {β : Sort v} [inst : Unique β] (e : α β) :

    If α ≃ β≃ β and β is a singleton type, then so is α.

    Equations
    def Equiv.cast {α : Sort u_1} {β : Sort u_1} (h : α = β) :
    α β

    Equivalence between equal types.

    Equations
    @[simp]
    theorem Equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : αβ) (g : βα) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) :
    ↑(Equiv.symm { toFun := f, invFun := g, left_inv := l, right_inv := r }) = g
    @[simp]
    theorem Equiv.coe_refl {α : Sort u} :
    ↑(Equiv.refl α) = id
    theorem Equiv.Perm.coe_subsingleton {α : Type u_1} [inst : Subsingleton α] (e : Equiv.Perm α) :
    e = id

    This cannot be a simp lemmas as it incorrectly matches against e : α ≃ synonym α≃ synonym α, when synonym α is semireducible. This makes a mess of multiplicative.of_add etc.

    @[simp]
    theorem Equiv.refl_apply {α : Sort u} (x : α) :
    ↑(Equiv.refl α) x = x
    @[simp]
    theorem Equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) :
    ↑(Equiv.trans f g) = g f
    @[simp]
    theorem Equiv.trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : α) :
    ↑(Equiv.trans f g) a = g (f a)
    @[simp]
    theorem Equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α β) (x : β) :
    e (↑(Equiv.symm e) x) = x
    @[simp]
    theorem Equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
    ↑(Equiv.symm e) (e x) = x
    @[simp]
    theorem Equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α β) :
    ↑(Equiv.symm e) e = id
    @[simp]
    theorem Equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α β) :
    e ↑(Equiv.symm e) = id
    @[simp]
    theorem Equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : γ) :
    ↑(Equiv.symm (Equiv.trans f g)) a = ↑(Equiv.symm f) (↑(Equiv.symm g) a)
    @[simp]
    theorem Equiv.symm_symm_apply {α : Sort u} {β : Sort v} (f : α β) (b : α) :
    ↑(Equiv.symm (Equiv.symm f)) b = f b
    theorem Equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α β) {x : α} {y : α} :
    f x = f y x = y
    theorem Equiv.apply_eq_iff_eq_symm_apply {α : Sort u} {β : Sort v} {x : α} {y : (fun x => β) x} (f : α β) :
    f x = y x = ↑(Equiv.symm f) y
    @[simp]
    theorem Equiv.cast_apply {α : Sort u_1} {β : Sort u_1} (h : α = β) (x : α) :
    ↑(Equiv.cast h) x = cast h x
    @[simp]
    theorem Equiv.cast_symm {α : Sort u_1} {β : Sort u_1} (h : α = β) :
    @[simp]
    theorem Equiv.cast_refl {α : Sort u_1} (h : optParam (α = α) (_ : α = α)) :
    @[simp]
    theorem Equiv.cast_trans {α : Sort u_1} {β : Sort u_1} {γ : Sort u_1} (h : α = β) (h2 : β = γ) :
    theorem Equiv.cast_eq_iff_heq {α : Sort u_1} {β : Sort u_1} (h : α = β) {a : α} {b : β} :
    ↑(Equiv.cast h) a = b HEq a b
    theorem Equiv.symm_apply_eq {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : (fun x => α) x} :
    ↑(Equiv.symm e) x = y x = e y
    theorem Equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : (fun x => α) x} :
    y = ↑(Equiv.symm e) x e y = x
    @[simp]
    theorem Equiv.symm_symm {α : Sort u} {β : Sort v} (e : α β) :
    @[simp]
    theorem Equiv.trans_refl {α : Sort u} {β : Sort v} (e : α β) :
    @[simp]
    theorem Equiv.refl_trans {α : Sort u} {β : Sort v} (e : α β) :
    @[simp]
    theorem Equiv.symm_trans_self {α : Sort u} {β : Sort v} (e : α β) :
    @[simp]
    theorem Equiv.self_trans_symm {α : Sort u} {β : Sort v} (e : α β) :
    theorem Equiv.trans_assoc {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (bc : β γ) (cd : γ δ) :
    theorem Equiv.leftInverse_symm {α : Sort u} {β : Sort v} (f : α β) :
    theorem Equiv.rightInverse_symm {α : Sort u} {β : Sort v} (f : α β) :
    theorem Equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : βγ) :
    theorem Equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : αβ) (e : β γ) :
    theorem Equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : βγ) :
    theorem Equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : αβ) (e : β γ) :
    theorem Equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : βγ) :
    theorem Equiv.comp_bijective {α : Sort u} {β : Sort v} {γ : Sort w} (f : αβ) (e : β γ) :
    def Equiv.equivCongr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
    α γ (β δ)

    If α is equivalent to β and γ is equivalent to δ, then the type of equivalences α ≃ γ≃ γ is equivalent to the type of equivalences β ≃ δ≃ δ.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.equivCongr_refl {α : Sort u_1} {β : Sort u_2} :
    @[simp]
    theorem Equiv.equivCongr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
    @[simp]
    theorem Equiv.equivCongr_trans {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α β) (de : δ ε) (bc : β γ) (ef : ε ζ) :
    @[simp]
    theorem Equiv.equivCongr_refl_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β γ) (e : α β) :
    @[simp]
    theorem Equiv.equivCongr_refl_right {α : Sort u_1} {β : Sort u_2} (ab : α β) (e : α β) :
    @[simp]
    theorem Equiv.equivCongr_apply_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) (e : α γ) (x : β) :
    ↑(↑(Equiv.equivCongr ab cd) e) x = cd (e (↑(Equiv.symm ab) x))
    def Equiv.permCongr {α' : Type u_1} {β' : Type u_2} (e : α' β') :

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

    Equations
    theorem Equiv.permCongr_def {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') :
    @[simp]
    theorem Equiv.permCongr_refl {α' : Type u_2} {β' : Type u_1} (e : α' β') :
    @[simp]
    theorem Equiv.permCongr_symm {α' : Type u_1} {β' : Type u_2} (e : α' β') :
    @[simp]
    theorem Equiv.permCongr_apply {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') (x : β') :
    ↑(↑(Equiv.permCongr e) p) x = e (p (↑(Equiv.symm e) x))
    theorem Equiv.permCongr_symm_apply {α' : Type u_2} {β' : Type u_1} (e : α' β') (p : Equiv.Perm β') (x : α') :
    ↑(↑(Equiv.symm (Equiv.permCongr e)) p) x = ↑(Equiv.symm e) (p (e x))
    theorem Equiv.permCongr_trans {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : Equiv.Perm α') (p' : Equiv.Perm α') :
    def Equiv.equivOfIsEmpty (α : Sort u_1) (β : Sort u_2) [inst : IsEmpty α] [inst : IsEmpty β] :
    α β

    Two empty types are equivalent.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.equivEmpty (α : Sort u) [inst : IsEmpty α] :

    If α is an empty type, then it is equivalent to the Empty type.

    Equations
    def Equiv.equivPEmpty (α : Sort v) [inst : IsEmpty α] :

    If α is an empty type, then it is equivalent to the PEmpty type in any universe.

    Equations

    α is equivalent to an empty type iff α is empty.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.propEquivPEmpty {p : Prop} (h : ¬p) :

    The Sort of proofs of a false proposition is equivalent to PEmpty.

    Equations
    def Equiv.equivOfUnique (α : Sort u) (β : Sort v) [inst : Unique α] [inst : Unique β] :
    α β

    If both α and β have a unique element, then α ≃ β≃ β.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.equivPUnit (α : Sort u) [inst : Unique α] :

    If α has a unique element, then it is equivalent to any PUnit.

    Equations
    def Equiv.propEquivPUnit {p : Prop} (h : p) :

    The Sort of proofs of a true proposition is equivalent to PUnit.

    Equations
    @[simp]
    theorem Equiv.ulift_apply {α : Type v} :
    Equiv.ulift = ULift.down
    def Equiv.ulift {α : Type v} :
    ULift α α

    ULift α is equivalent to α.

    Equations
    • Equiv.ulift = { toFun := ULift.down, invFun := ULift.up, left_inv := (_ : ∀ (b : ULift α), { down := b.down } = b), right_inv := (_ : ∀ (x : α), { down := x }.down = { down := x }.down) }
    @[simp]
    theorem Equiv.plift_apply {α : Sort u} :
    Equiv.plift = PLift.down
    def Equiv.plift {α : Sort u} :
    PLift α α

    PLift α is equivalent to α.

    Equations
    • Equiv.plift = { toFun := PLift.down, invFun := PLift.up, left_inv := (_ : ∀ (b : PLift α), { down := b.down } = b), right_inv := (_ : ∀ (a : α), { down := a }.down = a) }
    def Equiv.ofIff {P : Prop} {Q : Prop} (h : P Q) :
    P Q

    equivalence of propositions is the same as iff

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.arrowCongr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁β₁) :
    ∀ (a : α₂), ↑(Equiv.arrowCongr e₁ e₂) f a = (e₂ f ↑(Equiv.symm e₁)) a
    def Equiv.arrowCongr {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
    (α₁β₁) (α₂β₂)

    If α₁ is equivalent to α₂ and β₁ is equivalent to β₂, then the type of maps α₁ → β₁→ β₁ is equivalent to the type of maps α₂ → β₂→ β₂.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Equiv.arrowCongr_comp {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁β₁) (g : β₁γ₁) :
    ↑(Equiv.arrowCongr ea ec) (g f) = ↑(Equiv.arrowCongr eb ec) g ↑(Equiv.arrowCongr ea eb) f
    @[simp]
    theorem Equiv.arrowCongr_refl {α : Sort u_1} {β : Sort u_2} :
    @[simp]
    theorem Equiv.arrowCongr_trans {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
    Equiv.arrowCongr (Equiv.trans e₁ e₂) (Equiv.trans e₁' e₂') = Equiv.trans (Equiv.arrowCongr e₁ e₁') (Equiv.arrowCongr e₂ e₂')
    @[simp]
    theorem Equiv.arrowCongr_symm {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
    @[simp]
    theorem Equiv.arrowCongr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) (f : α₁β₁) :
    ∀ (a : α₂), ↑(Equiv.arrowCongr' ) f a = (f (↑(Equiv.symm ) a))
    def Equiv.arrowCongr' {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) :
    (α₁β₁) (α₂β₂)

    A version of Equiv.arrowCongr in Type, rather than Sort.

    The equiv_rw tactic is not able to use the default Sort level Equiv.arrowCongr, because Lean's universe rules will not unify ?l_1 with imax (1 ?m_1).

    Equations
    @[simp]
    theorem Equiv.arrowCongr'_refl {α : Type u_1} {β : Type u_2} :
    @[simp]
    theorem Equiv.arrowCongr'_trans {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
    Equiv.arrowCongr' (Equiv.trans e₁ e₂) (Equiv.trans e₁' e₂') = Equiv.trans (Equiv.arrowCongr' e₁ e₁') (Equiv.arrowCongr' e₂ e₂')
    @[simp]
    theorem Equiv.arrowCongr'_symm {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
    @[simp]
    theorem Equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : αα) :
    ∀ (a : β), ↑(Equiv.conj e) f a = e (f (↑(Equiv.symm e) a))
    def Equiv.conj {α : Sort u} {β : Sort v} (e : α β) :
    (αα) (ββ)

    Conjugate a map f : α → α→ α by an equivalence α ≃ β≃ β.

    Equations
    @[simp]
    theorem Equiv.conj_refl {α : Sort u} :
    @[simp]
    theorem Equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :
    @[simp]
    theorem Equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
    theorem Equiv.conj_comp {α : Sort u} {β : Sort v} (e : α β) (f₁ : αα) (f₂ : αα) :
    ↑(Equiv.conj e) (f₁ f₂) = ↑(Equiv.conj e) f₁ ↑(Equiv.conj e) f₂
    theorem Equiv.eq_comp_symm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : βγ) (g : αγ) :
    f = g ↑(Equiv.symm e) f e = g
    theorem Equiv.comp_symm_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : βγ) (g : αγ) :
    g ↑(Equiv.symm e) = f g = f e
    theorem Equiv.eq_symm_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : γα) (g : γβ) :
    f = ↑(Equiv.symm e) g e f = g
    theorem Equiv.symm_comp_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α β) (f : γα) (g : γβ) :
    ↑(Equiv.symm e) g = f g = e f

    PUnit sorts in any two universes are equivalent.

    Equations
    noncomputable def Equiv.propEquivBool :

    Prop is noncomputably equivalent to Bool.

    Equations
    def Equiv.arrowPUnitEquivPUnit (α : Sort u_1) :
    (αPUnit) PUnit

    The sort of maps to PUnit.{v} is equivalent to PUnit.{w}.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.piSubsingleton_symm_apply {α : Sort u} (β : αSort u_1) [inst : Subsingleton α] (a : α) (x : β a) (b : α) :
    ↑(Equiv.symm (Equiv.piSubsingleton β a)) x b = cast (_ : β a = β b) x
    @[simp]
    theorem Equiv.piSubsingleton_apply {α : Sort u} (β : αSort u_1) [inst : Subsingleton α] (a : α) (f : (x : α) → β x) :
    def Equiv.piSubsingleton {α : Sort u} (β : αSort u_1) [inst : Subsingleton α] (a : α) :
    ((a' : α) → β a') β a

    If α is Subsingleton and a : α, then the type of dependent functions Π (i : α), β i is equivalent to β a.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.funUnique_apply (α : Sort u) (β : Sort u_1) [inst : Unique α] :
    ↑(Equiv.funUnique α β) = fun f => f default
    def Equiv.funUnique (α : Sort u) (β : Sort u_1) [inst : Unique α] :
    (αβ) β

    If α has a unique term, then the type of function α → β→ β is equivalent to β.

    Equations
    def Equiv.punitArrowEquiv (α : Sort u_1) :
    (PUnitα) α

    The sort of maps from PUnit is equivalent to the codomain.

    Equations
    def Equiv.trueArrowEquiv (α : Sort u_1) :
    (Trueα) α

    The sort of maps from True is equivalent to the codomain.

    Equations
    def Equiv.arrowPUnitOfIsEmpty (α : Sort u_1) (β : Sort u_2) [inst : IsEmpty α] :
    (αβ) PUnit

    The sort of maps from a type that IsEmpty is equivalent to PUnit.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.emptyArrowEquivPUnit (α : Sort u_1) :
    (Emptyα) PUnit

    The sort of maps from Empty is equivalent to PUnit.

    Equations

    The sort of maps from PEmpty is equivalent to PUnit.

    Equations
    def Equiv.falseArrowEquivPUnit (α : Sort u_1) :
    (Falseα) PUnit

    The sort of maps from False is equivalent to PUnit.

    Equations
    @[simp]
    theorem Equiv.psigmaEquivSigma_symm_apply {α : Type u_1} (β : αType u_2) (a : (i : α) × β i) :
    ↑(Equiv.symm (Equiv.psigmaEquivSigma β)) a = { fst := a.fst, snd := a.snd }
    @[simp]
    theorem Equiv.psigmaEquivSigma_apply {α : Type u_1} (β : αType u_2) (a : (i : α) ×' β i) :
    ↑(Equiv.psigmaEquivSigma β) a = { fst := a.fst, snd := a.snd }
    def Equiv.psigmaEquivSigma {α : Type u_1} (β : αType u_2) :
    (i : α) ×' β i (i : α) × β i

    A PSigma-type is equivalent to the corresponding Sigma-type.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.psigmaEquivSigmaPLift_symm_apply {α : Sort u_1} (β : αSort u_2) (a : (i : PLift α) × PLift (β i.down)) :
    ↑(Equiv.symm (Equiv.psigmaEquivSigmaPLift β)) a = { fst := a.fst.down, snd := a.snd.down }
    @[simp]
    theorem Equiv.psigmaEquivSigmaPLift_apply {α : Sort u_1} (β : αSort u_2) (a : (i : α) ×' β i) :
    ↑(Equiv.psigmaEquivSigmaPLift β) a = { fst := { down := a.fst }, snd := { down := a.snd } }
    def Equiv.psigmaEquivSigmaPLift {α : Sort u_1} (β : αSort u_2) :
    (i : α) ×' β i (i : PLift α) × PLift (β i.down)

    A PSigma-type is equivalent to the corresponding Sigma-type.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Equiv.psigmaCongrRight_apply {α : Sort u} {β₁ : αSort u_1} {β₂ : αSort u_2} (F : (a : α) → β₁ a β₂ a) (a : (a : α) ×' β₁ a) :
    ↑(Equiv.psigmaCongrRight F) a = { fst := a.fst, snd := ↑(F a.fst) a.snd }
    def Equiv.psigmaCongrRight {α : Sort u} {β₁ : αSort u_1} {β₂ : αSort u_2} (F : (a : α) → β₁ a β₂ a) :
    (a : α) ×' β₁ a (a : α) ×' β₂ a

    A family of equivalences Π a, β₁ a ≃ β₂ a≃ β₂ a generates an equivalence between Σ' a, β₁ a and Σ' a, β₂ a.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Equiv.psigmaCongrRight_trans {α : Sort u_1} {β₁ : αSort u_2} {β₂ : αSort u_3} {β₃ : αSort u_4} (F : (a : α) → β₁ a β₂ a) (G : (a : α) → β₂ a β₃ a) :
    theorem Equiv.psigmaCongrRight_symm {α : Sort u_1} {β₁ : αSort u_2} {β₂ : αSort u_3} (F : (a : α) → β₁ a β₂ a) :
    theorem Equiv.psigmaCongrRight_refl {α : Sort u_1} {β : αSort u_2} :
    (Equiv.psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)
    @[simp]
    theorem Equiv.sigmaCongrRight_apply {α : Type u_1} {β₁ : αType u_2} {β₂ : αType u_3} (F : (a : α) → β₁ a β₂ a) (a : (a : α) × β₁ a) :
    ↑(Equiv.sigmaCongrRight F) a = { fst := a.fst, snd := ↑(F a.fst) a.snd }
    def Equiv.sigmaCongrRight {α : Type u_1} {β₁ : αType u_2} {β₂ : αType u_3} (F : (a : α) → β₁ a β₂ a) :
    (a : α) × β₁ a (a : α) × β₂ a

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Equiv.sigmaCongrRight_trans {α : Type u_1} {β₁ : αType u_2} {β₂ : αType u_3} {β₃ : αType u_4} (F : (a : α) → β₁ a β₂ a) (G : (a : α) → β₂ a β₃ a) :
    theorem Equiv.sigmaCongrRight_symm {α : Type u_1} {β₁ : αType u_2} {β₂ : αType u_3} (F : (a : α) → β₁ a β₂ a) :
    theorem Equiv.sigmaCongrRight_refl {α : Type u_1} {β : αType u_2} :
    (Equiv.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
    def Equiv.psigmaEquivSubtype {α : Type v} (P : αProp) :
    (i : α) ×' P i Subtype P

    A PSigma with Prop fibers is equivalent to the subtype.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.sigmaPLiftEquivSubtype {α : Type v} (P : αProp) :
    (i : α) × PLift (P i) Subtype P

    A Sigma with PLift fibers is equivalent to the subtype.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.sigmaULiftPLiftEquivSubtype {α : Type v} (P : αProp) :
    (i : α) × ULift (PLift (P i)) Subtype P

    A Sigma with λ i, ULift (PLift (P i)) fibers is equivalent to { x // P x }. Variant of sigmaPLiftEquivSubtype.

    Equations
    def Equiv.Perm.sigmaCongrRight {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) :
    Equiv.Perm ((a : α) × β a)

    A family of permutations Π a, Perm (β a) generates a permuation Perm (Σ a, β₁ a).

    Equations
    @[simp]
    theorem Equiv.Perm.sigmaCongrRight_trans {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) (G : (a : α) → Equiv.Perm (β a)) :
    @[simp]
    theorem Equiv.Perm.sigmaCongrRight_symm {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) :
    @[simp]
    theorem Equiv.Perm.sigmaCongrRight_refl {α : Type u_1} {β : αType u_2} :
    (Equiv.Perm.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
    @[simp]
    theorem Equiv.sigmaCongrLeft_apply {α₂ : Type u_1} {α₁ : Type u_2} {β : α₂Type u_3} (e : α₁ α₂) (a : (a : α₁) × β (e a)) :
    ↑(Equiv.sigmaCongrLeft e) a = { fst := e a.fst, snd := a.snd }
    def Equiv.sigmaCongrLeft {α₂ : Type u_1} {α₁ : Type u_2} {β : α₂Type u_3} (e : α₁ α₂) :
    (a : α₁) × β (e a) (a : α₂) × β a

    An equivalence f : α₁ ≃ α₂≃ α₂ generates an equivalence between Σ a, β (f a) and Σ a, β a.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.sigmaCongrLeft' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁Type u_3} (f : α₁ α₂) :
    (a : α₁) × β a (a : α₂) × β (↑(Equiv.symm f) a)

    Transporting a sigma type through an equivalence of the base

    Equations
    def Equiv.sigmaCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁Type u_3} {β₂ : α₂Type u_4} (f : α₁ α₂) (F : (a : α₁) → β₁ a β₂ (f a)) :
    Sigma β₁ Sigma β₂

    Transporting a sigma type through an equivalence of the base and a family of equivalences of matching fibers

    Equations
    @[simp]
    theorem Equiv.sigmaEquivProd_apply (α : Type u_1) (β : Type u_2) (a : (_ : α) × β) :
    ↑(Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
    @[simp]
    theorem Equiv.sigmaEquivProd_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :
    ↑(Equiv.symm (Equiv.sigmaEquivProd α β)) a = { fst := a.fst, snd := a.snd }
    def Equiv.sigmaEquivProd (α : Type u_1) (β : Type u_2) :
    (_ : α) × β α × β

    Sigma type with a constant fiber is equivalent to the product.

    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.sigmaEquivProdOfEquiv {α : Type u_1} {β : Type u_2} {β₁ : αType u_3} (F : (a : α) → β₁ a β) :
    Sigma β₁ α × β

    If each fiber of a Sigma type is equivalent to a fixed type, then the sigma type is equivalent to the product.

    Equations
    def Equiv.sigmaAssoc {α : Type u_1} {β : αType u_2} (γ : (a : α) → β aType u_3) :
    (ab : (a : α) × β a) × γ ab.fst ab.snd (a : α) × (b : β a) × γ a b

    Dependent product of types is associative up to an equivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Equiv.exists_unique_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (f : α β) (h : ∀ {x : α}, p x q (f x)) :
    (∃! x, p x) ∃! y, q y
    theorem Equiv.exists_unique_congr_left' {α : Sort u} {β : Sort v} {p : αProp} (f : α β) :
    (∃! x, p x) ∃! y, p (↑(Equiv.symm f) y)
    theorem Equiv.exists_unique_congr_left {α : Sort u} {β : Sort v} {p : βProp} (f : α β) :
    (∃! x, p (f x)) ∃! y, p y
    theorem Equiv.forall_congr {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (f : α β) (h : ∀ {x : α}, p x q (f x)) :
    ((x : α) → p x) (y : β) → q y
    theorem Equiv.forall_congr' {α : Sort u} {β : Sort v} {p : αProp} {q : βProp} (f : α β) (h : ∀ {x : β}, p (↑(Equiv.symm f) x) q x) :
    ((x : α) → p x) (y : β) → q y
    theorem Equiv.forall₂_congr {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {p : α₁β₁Prop} {q : α₂β₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (h : ∀ {x : α₁} {y : β₁}, p x y q ( x) ( y)) :
    ((x : α₁) → (y : β₁) → p x y) (x : α₂) → (y : β₂) → q x y
    theorem Equiv.forall₂_congr' {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {p : α₁β₁Prop} {q : α₂β₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (h : ∀ {x : α₂} {y : β₂}, p (↑(Equiv.symm ) x) (↑(Equiv.symm ) y) q x y) :
    ((x : α₁) → (y : β₁) → p x y) (x : α₂) → (y : β₂) → q x y
    theorem Equiv.forall₃_congr {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} {p : α₁β₁γ₁Prop} {q : α₂β₂γ₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) (h : ∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z q ( x) ( y) ( z)) :
    ((x : α₁) → (y : β₁) → (z : γ₁) → p x y z) (x : α₂) → (y : β₂) → (z : γ₂) → q x y z
    theorem Equiv.forall₃_congr' {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} {p : α₁β₁γ₁Prop} {q : α₂β₂γ₂Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) (h : ∀ {x : α₂} {y : β₂} {z : γ₂}, p (↑(Equiv.symm ) x) (↑(Equiv.symm ) y) (↑(Equiv.symm ) z) q x y z) :
    ((x : α₁) → (y : β₁) → (z : γ₁) → p x y z) (x : α₂) → (y : β₂) → (z : γ₂) → q x y z
    theorem Equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : αProp} (f : α β) :
    ((x : α) → p x) (y : β) → p (↑(Equiv.symm f) y)
    theorem Equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : βProp} (f : α β) :
    ((x : α) → p (f x)) (y : β) → p y
    theorem Equiv.exists_congr_left {α : Sort u_1} {β : Sort u_2} (f : α β) {p : αProp} :
    (a, p a) b, p (↑(Equiv.symm f) b)
    def Quot.congr {α : Sort u} {β : Sort v} {ra : ααProp} {rb : ββProp} (e : α β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) :
    Quot ra Quot rb

    An equivalence e : α ≃ β≃ β generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Quot.congr_mk {α : Sort u} {β : Sort v} {ra : ααProp} {rb : ββProp} (e : α β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂)) (a : α) :
    ↑(Quot.congr e eq) (Quot.mk ra a) = Quot.mk rb (e a)
    def Quot.congrRight {α : Sort u} {r : ααProp} {r' : ααProp} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ r' a₁ a₂) :

    Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

    Equations
    def Quot.congrLeft {α : Sort u} {β : Sort v} {r : ααProp} (e : α β) :
    Quot r Quot fun b b' => r (↑(Equiv.symm e) b) (↑(Equiv.symm e) b')

    An equivalence e : α ≃ β≃ β generates an equivalence between the quotient space of α by a relation ra and the quotient space of β by the image of this relation under e.

    Equations
    def Quotient.congr {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α β) (eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ Setoid.r (e a₁) (e a₂)) :

    An equivalence e : α ≃ β≃ β generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

    Equations
    @[simp]
    theorem Quotient.congr_mk {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α β) (eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ Setoid.r (e a₁) (e a₂)) (a : α) :
    ↑(Quotient.congr e eq) (Quotient.mk ra a) = Quotient.mk rb (e a)
    def Quotient.congrRight {α : Sort u} {r : Setoid α} {r' : Setoid α} (eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ Setoid.r a₁ a₂) :

    Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

    Equations