Equivalence between types

In this file we define two types:

• Equiv α β a.k.a. α ≃ β: a bijective map α → β bundled with its inverse map; we use this (and not equality!) to express that various Types or Sorts are equivalent.

• Equiv.Perm α: the group of permutations α ≃ α. More lemmas about Equiv.Perm can be found in Mathlib/GroupTheory/Perm.lean.

Then we define

• canonical isomorphisms between various types: e.g.,

  • Equiv.refl α is the identity map interpreted as α ≃ α;

• operations on equivalences: e.g.,

  • Equiv.symm e : β ≃ α is the inverse of e : α ≃ β;

  • Equiv.trans e₁ e₂ : α ≃ γ is the composition of e₁ : α ≃ β and e₂ : β ≃ γ (note the order of the arguments!);

• definitions that transfer some instances along an equivalence. By convention, we transfer instances from right to left.

  • Equiv.inhabited takes e : α ≃ β and [Inhabited β] and returns Inhabited α;
  • Equiv.unique takes e : α ≃ β and [Unique β] and returns Unique α;
  • Equiv.decidableEq takes e : α ≃ β and [DecidableEq β] and returns DecidableEq α.

  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.

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

Tags

equivalence, congruence, bijective map

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

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

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun

def «term_≃_» : Lean.TrailingParserDescr

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

Equations

• «term_≃_» = Lean.ParserDescr.trailingNode `«term_≃_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ ") (Lean.ParserDescr.cat `term 26))

def EquivLike.toEquiv {α : Sort u} {β : Sort v} {F : Sort u_1} [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

• ↑f = { toFun := ⇑f, invFun := EquivLike.inv f, left_inv := ⋯, right_inv := ⋯ }

instance instCoeTCEquivOfEquivLike {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] : CoeTC F (α ≃ β)

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

Equations

• instCoeTCEquivOfEquivLike = { coe := EquivLike.toEquiv }

@[reducible, inline]

abbrev Equiv.Perm (α : Sort u_1) : Sort (max 1 u_1)

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

Equations

• Equiv.Perm α = (α ≃ α)

instance Equiv.instEquivLike {α : Sort u} {β : Sort v} : EquivLike (α ≃ β) α β

Equations

• Equiv.instEquivLike = { coe := Equiv.toFun, inv := Equiv.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance Equiv.instFunLike {α : Sort u} {β : Sort v} : FunLike (α ≃ β) α β

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

TODO: this instance doesn't appear to be necessary: remove it (after benchmarking?)

Equations

• Equiv.instFunLike = { coe := Equiv.toFun, coe_injective' := ⋯ }

@[simp]

theorem EquivLike.coe_coe {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) : ⇑↑e = ⇑e

@[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) 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.ext_iff {α : Sort u} {β : Sort v} {f g : α ≃ β} : f = g ↔ ∀ (x : α), f x = g x

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.Perm.ext {α : Sort u} {σ τ : Perm α} (H : ∀ (x : α), σ x = τ x) : σ = τ

theorem Equiv.Perm.ext_iff {α : Sort u} {σ τ : Perm α} : σ = τ ↔ ∀ (x : α), σ x = τ x

theorem Equiv.Perm.congr_arg {α : Sort u} {f : Perm α} {x x' : α} : x = x' → f x = f x'

theorem Equiv.Perm.congr_fun {α : Sort u} {f g : Perm α} (h : f = g) (x : α) : f x = g x

def Equiv.refl (α : Sort u_1) : α ≃ α

Any type is equivalent to itself.

Equations

• Equiv.refl α = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ }

instance Equiv.inhabited' {α : Sort u} : Inhabited (α ≃ α)

Equations

• Equiv.inhabited' = { default := Equiv.refl α }

def Equiv.symm {α : Sort u} {β : Sort v} (e : α ≃ β) : β ≃ α

Inverse of an equivalence e : α ≃ β.

Equations

• e.symm = { toFun := e.invFun, invFun := e.toFun, left_inv := ⋯, right_inv := ⋯ }

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

See Note [custom simps projection]

Equations

• Equiv.Simps.symm_apply e = ⇑e.symm

theorem Equiv.left_inv' {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.LeftInverse ⇑e.symm ⇑e

Restatement of Equiv.left_inv in terms of Function.LeftInverse.

theorem Equiv.right_inv' {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.RightInverse ⇑e.symm ⇑e

Restatement of Equiv.right_inv in terms of Function.RightInverse.

def Equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ

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

Equations

• e₁.trans e₂ = { toFun := ⇑e₂ ∘ ⇑e₁, invFun := ⇑e₁.symm ∘ ⇑e₂.symm, left_inv := ⋯, right_inv := ⋯ }

instance Equiv.instTrans : Trans Equiv Equiv Equiv

Equations

• Equiv.instTrans = { trans := fun {a : Sort ?u.12} {b : Sort ?u.13} {c : Sort ?u.11} => Equiv.trans }

@[simp]

theorem Equiv.trans_def {a✝ : Sort u_2} {b✝ : Sort u_1} {c✝ : Sort u_3} (e₁ : a✝ ≃ b✝) (e₂ : b✝ ≃ c✝) : Trans.trans e₁ e₂ = e₁.trans e₂

@[simp]

theorem Equiv.toFun_as_coe {α : Sort u} {β : Sort v} (e : α ≃ β) : e.toFun = ⇑e

@[simp]

theorem Equiv.invFun_as_coe {α : Sort u} {β : Sort v} (e : α ≃ β) : e.invFun = ⇑e.symm

theorem Equiv.injective {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Injective ⇑e

theorem Equiv.surjective {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Surjective ⇑e

theorem Equiv.bijective {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Bijective ⇑e

theorem Equiv.subsingleton {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton β] : Subsingleton α

theorem Equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton α] : Subsingleton β

theorem Equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α ≃ β) : Subsingleton α ↔ Subsingleton β

instance Equiv.equiv_subsingleton_cod {α : Sort u} {β : Sort v} [Subsingleton β] : Subsingleton (α ≃ β)

instance Equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [Subsingleton α] : Subsingleton (α ≃ β)

instance Equiv.permUnique {α : Sort u} [Subsingleton α] : Unique (Perm α)

Equations

• Equiv.permUnique = uniqueOfSubsingleton (Equiv.refl α)

theorem Equiv.Perm.subsingleton_eq_refl {α : Sort u} [Subsingleton α] (e : Perm α) : e = Equiv.refl α

theorem Equiv.nontrivial {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Nontrivial β] : Nontrivial α

theorem Equiv.nontrivial_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Nontrivial α ↔ Nontrivial β

def Equiv.decidableEq {α : Sort u} {β : Sort v} (e : α ≃ β) [DecidableEq β] : DecidableEq α

Transfer DecidableEq across an equivalence.

Equations

• e.decidableEq = ⋯.decidableEq

theorem Equiv.nonempty_congr {α : Sort u} {β : Sort v} (e : α ≃ β) : Nonempty α ↔ Nonempty β

theorem Equiv.nonempty {α : Sort u} {β : Sort v} (e : α ≃ β) [Nonempty β] : Nonempty α

def Equiv.inhabited {α : Sort u} {β : Sort v} [Inhabited β] (e : α ≃ β) : Inhabited α

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

Equations

• e.inhabited = { default := e.symm default }

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

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

Equations

• e.unique = Function.Surjective.unique ⇑e.symm ⋯

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

Equivalence between equal types.

Equations

• Equiv.cast h = { toFun := cast h, invFun := cast ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.coe_fn_symm_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 }.symm = g

@[simp]

theorem Equiv.coe_refl {α : Sort u} : ⇑(Equiv.refl α) = id

theorem Equiv.Perm.coe_subsingleton {α : Type u_1} [Subsingleton α] (e : Perm α) : ⇑e = id

This cannot be a simp lemmas as it incorrectly matches against e : α ≃ synonym α, when synonym α is semireducible. This makes a mess of Multiplicative.ofAdd 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 : β ≃ γ) : ⇑(f.trans g) = ⇑g ∘ ⇑f

@[simp]

theorem Equiv.trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a)

@[simp]

theorem Equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β) : e (e.symm x) = x

@[simp]

theorem Equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α) : e.symm (e x) = x

@[simp]

theorem Equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α ≃ β) : ⇑e.symm ∘ ⇑e = id

@[simp]

theorem Equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α ≃ β) : ⇑e ∘ ⇑e.symm = id

@[simp]

theorem EquivLike.apply_coe_symm_apply {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : β) : e ((↑e).symm x) = x

@[simp]

theorem EquivLike.coe_symm_apply_apply {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : α) : (↑e).symm (e x) = x

@[simp]

theorem EquivLike.coe_symm_comp_self {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) : ⇑(↑e).symm ∘ ⇑e = id

@[simp]

theorem EquivLike.self_comp_coe_symm {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) : ⇑e ∘ ⇑(↑e).symm = id

@[simp]

theorem Equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : γ) : (f.trans g).symm a = f.symm (g.symm a)

theorem Equiv.symm_symm_apply {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α) : f.symm.symm 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 : β} (f : α ≃ β) : f x = y ↔ x = f.symm y

@[simp]

theorem Equiv.cast_apply {α β : Sort u_1} (h : α = β) (x : α) : (Equiv.cast h) x = cast h x

@[simp]

theorem Equiv.cast_symm {α β : Sort u_1} (h : α = β) : (Equiv.cast h).symm = Equiv.cast ⋯

@[simp]

theorem Equiv.cast_refl {α : Sort u_1} (h : α = α := ⋯) : Equiv.cast h = Equiv.refl α

@[simp]

theorem Equiv.cast_trans {α β γ : Sort u_1} (h : α = β) (h2 : β = γ) : (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast ⋯

theorem Equiv.cast_eq_iff_heq {α β : Sort u_1} (h : α = β) {a : α} {b : β} : (Equiv.cast h) a = b ↔ a ≍ b

theorem Equiv.symm_apply_eq {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} : e.symm x = y ↔ x = e y

theorem Equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} : y = e.symm x ↔ e y = x

@[simp]

theorem Equiv.symm_symm {α : Sort u} {β : Sort v} (e : α ≃ β) : e.symm.symm = e

theorem Equiv.symm_bijective {α : Sort u} {β : Sort v} : Function.Bijective Equiv.symm

@[simp]

theorem Equiv.trans_refl {α : Sort u} {β : Sort v} (e : α ≃ β) : e.trans (Equiv.refl β) = e

@[simp]

theorem Equiv.refl_symm {α : Sort u} : (Equiv.refl α).symm = Equiv.refl α

@[simp]

theorem Equiv.refl_trans {α : Sort u} {β : Sort v} (e : α ≃ β) : (Equiv.refl α).trans e = e

@[simp]

theorem Equiv.symm_trans_self {α : Sort u} {β : Sort v} (e : α ≃ β) : e.symm.trans e = Equiv.refl β

@[simp]

theorem Equiv.self_trans_symm {α : Sort u} {β : Sort v} (e : α ≃ β) : e.trans e.symm = Equiv.refl α

theorem Equiv.trans_assoc {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) : (ab.trans bc).trans cd = ab.trans (bc.trans cd)

theorem Equiv.leftInverse_symm {α : Sort u} {β : Sort v} (f : α ≃ β) : Function.LeftInverse ⇑f.symm ⇑f

theorem Equiv.rightInverse_symm {α : Sort u} {β : Sort v} (f : α ≃ β) : Function.RightInverse ⇑f.symm ⇑f

theorem Equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) : Function.Injective (f ∘ ⇑e) ↔ Function.Injective f

theorem Equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) : Function.Injective (⇑e ∘ f) ↔ Function.Injective f

theorem Equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) : Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f

theorem Equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) : Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f

theorem Equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) : Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f

theorem Equiv.comp_bijective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) : Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f

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

• ab.equivCongr cd = { toFun := fun (ac : α ≃ γ) => (ab.symm.trans ac).trans cd, invFun := fun (bd : β ≃ δ) => ab.trans (bd.trans cd.symm), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.equivCongr_refl {α : Sort u_1} {β : Sort u_2} : (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

@[simp]

theorem Equiv.equivCongr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) : (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

@[simp]

theorem Equiv.equivCongr_trans {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α ≃ β) (de : δ ≃ ε) (bc : β ≃ γ) (ef : ε ≃ ζ) : (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

@[simp]

theorem Equiv.equivCongr_refl_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β ≃ γ) (e : α ≃ β) : ((Equiv.refl α).equivCongr bg) e = e.trans bg

@[simp]

theorem Equiv.equivCongr_refl_right {α : Sort u_1} {β : Sort u_2} (ab e : α ≃ β) : (ab.equivCongr (Equiv.refl β)) e = ab.symm.trans e

@[simp]

theorem Equiv.equivCongr_apply_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) (e : α ≃ γ) (x : β) : ((ab.equivCongr cd) e) x = cd (e (ab.symm x))

def Equiv.permCongr {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') : Perm α' ≃ Perm β'

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

Equations

• e.permCongr = e.equivCongr e

theorem Equiv.permCongr_def {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Perm α') : e.permCongr p = (e.symm.trans p).trans e

@[simp]

theorem Equiv.permCongr_refl {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') : e.permCongr (Equiv.refl α') = Equiv.refl β'

@[simp]

theorem Equiv.permCongr_symm {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') : e.permCongr.symm = e.symm.permCongr

@[simp]

theorem Equiv.permCongr_apply {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Perm α') (x : β') : (e.permCongr p) x = e (p (e.symm x))

theorem Equiv.permCongr_symm_apply {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Perm β') (x : α') : (e.permCongr.symm p) x = e.symm (p (e x))

theorem Equiv.permCongr_trans {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p p' : Perm α') : Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')

def Equiv.equivOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] [IsEmpty β] : α ≃ β

Two empty types are equivalent.

Equations

• Equiv.equivOfIsEmpty α β = { toFun := fun (a : α) => isEmptyElim a, invFun := fun (a : β) => isEmptyElim a, left_inv := ⋯, right_inv := ⋯ }

def Equiv.equivEmpty (α : Sort u) [IsEmpty α] : α ≃ Empty

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

Equations

• Equiv.equivEmpty α = Equiv.equivOfIsEmpty α Empty

def Equiv.equivPEmpty (α : Sort v) [IsEmpty α] : α ≃ PEmpty.{u}

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

Equations

• Equiv.equivPEmpty α = Equiv.equivOfIsEmpty α PEmpty.{?u.11}

def Equiv.equivEmptyEquiv (α : Sort u) : α ≃ Empty ≃ IsEmpty α

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

Equations

• Equiv.equivEmptyEquiv α = { toFun := ⋯, invFun := @Equiv.equivEmpty α, left_inv := ⋯, right_inv := ⋯ }

def Equiv.propEquivPEmpty {p : Prop} (h : ¬p) : p ≃ PEmpty.{u_1}

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

Equations

• Equiv.propEquivPEmpty h = Equiv.equivPEmpty p

def Equiv.ofUnique (α : Sort u) (β : Sort v) [Unique α] [Unique β] : α ≃ β

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

Equations

• Equiv.ofUnique α β = { toFun := default, invFun := default, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.ofUnique_symm_apply (α : Sort u) (β : Sort v) [Unique α] [Unique β] (a✝ : β) : (ofUnique α β).symm a✝ = default a✝

@[simp]

theorem Equiv.ofUnique_apply (α : Sort u) (β : Sort v) [Unique α] [Unique β] (a✝ : α) : (ofUnique α β) a✝ = default a✝

@[deprecated Equiv.ofUnique (since := "2024-12-26")]

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

Alias of Equiv.ofUnique.

---

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

Equations

• Equiv.equivOfUnique = Equiv.ofUnique

def Equiv.equivPUnit (α : Sort u) [Unique α] : α ≃ PUnit.{v}

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

Equations

• Equiv.equivPUnit α = Equiv.ofUnique α PUnit.{?u.10}

@[simp]

theorem Equiv.equivPUnit_symm_apply (α : Sort u) [Unique α] (a✝ : PUnit.{v}) : (equivPUnit α).symm a✝ = default

@[simp]

theorem Equiv.equivPUnit_apply (α : Sort u) [Unique α] (a✝ : α) : (equivPUnit α) a✝ = PUnit.unit

def Equiv.propEquivPUnit {p : Prop} (h : p) : p ≃ PUnit.{0}

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

Equations

• Equiv.propEquivPUnit h = Equiv.equivPUnit p

def Equiv.ulift {α : Type v} : ULift.{u, v} α ≃ α

ULift α is equivalent to α.

Equations

• Equiv.ulift = { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.ulift_apply {α : Type v} : ⇑Equiv.ulift = ULift.down

def Equiv.plift {α : Sort u} : PLift α ≃ α

PLift α is equivalent to α.

Equations

• Equiv.plift = { toFun := PLift.down, invFun := PLift.up, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.plift_apply {α : Sort u} : ⇑Equiv.plift = PLift.down

def Equiv.ofIff {P Q : Prop} (h : P ↔ Q) : P ≃ Q

equivalence of propositions is the same as iff

Equations

• Equiv.ofIff h = { toFun := ⋯, invFun := ⋯, left_inv := ⋯, right_inv := ⋯ }

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

• e₁.arrowCongr e₂ = { toFun := fun (f : α₁ → β₁) => ⇑e₂ ∘ f ∘ ⇑e₁.symm, invFun := fun (f : α₂ → β₂) => ⇑e₂.symm ∘ f ∘ ⇑e₁, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.arrowCongr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) (a✝ : α₂) : (e₁.arrowCongr e₂) f a✝ = (⇑e₂ ∘ f ∘ ⇑e₁.symm) a✝

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 : β₁ → γ₁) : (ea.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f

@[simp]

theorem Equiv.arrowCongr_refl {α : Sort u_1} {β : Sort u_2} : (Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (α → β)

@[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₂' : β₂ ≃ β₃) : (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')

@[simp]

theorem Equiv.arrowCongr_symm {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

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

• hα.arrowCongr' hβ = hα.arrowCongr hβ

@[simp]

theorem Equiv.arrowCongr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) (f : α₁ → β₁) (a✝ : α₂) : (hα.arrowCongr' hβ) f a✝ = hβ (f (hα.symm a✝))

@[simp]

theorem Equiv.arrowCongr'_refl {α : Type u_1} {β : Type u_2} : (Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.refl (α → β)

@[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₂' : β₂ ≃ β₃) : (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')

@[simp]

theorem Equiv.arrowCongr'_symm {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm

def Equiv.conj {α : Sort u} {β : Sort v} (e : α ≃ β) : (α → α) ≃ (β → β)

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

Equations

• e.conj = e.arrowCongr e

@[simp]

theorem Equiv.conj_apply {α : Sort u} {β : Sort v} (e : α ≃ β) (f : α → α) (a✝ : β) : e.conj f a✝ = e (f (e.symm a✝))

@[simp]

theorem Equiv.conj_refl {α : Sort u} : (Equiv.refl α).conj = Equiv.refl (α → α)

@[simp]

theorem Equiv.conj_symm {α : Sort u} {β : Sort v} (e : α ≃ β) : e.conj.symm = e.symm.conj

@[simp]

theorem Equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) : (e₁.trans e₂).conj = e₁.conj.trans e₂.conj

theorem Equiv.conj_comp {α : Sort u} {β : Sort v} (e : α ≃ β) (f₁ f₂ : α → α) : e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂

theorem Equiv.eq_comp_symm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem Equiv.comp_symm_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem Equiv.eq_symm_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem Equiv.symm_comp_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

theorem Equiv.trans_eq_refl_iff_eq_symm {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f = g.symm

theorem Equiv.trans_eq_refl_iff_symm_eq {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f.symm = g

theorem Equiv.eq_symm_iff_trans_eq_refl {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f = g.symm ↔ f.trans g = Equiv.refl α

theorem Equiv.symm_eq_iff_trans_eq_refl {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f.symm = g ↔ f.trans g = Equiv.refl α

def Equiv.punitEquivPUnit : PUnit.{v} ≃ PUnit.{w}

PUnit sorts in any two universes are equivalent.

Equations

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

noncomputable def Equiv.propEquivBool : Prop ≃ Bool

Prop is noncomputably equivalent to Bool.

Equations

• Equiv.propEquivBool = { toFun := fun (p : Prop) => decide p, invFun := fun (b : Bool) => b = true, left_inv := Equiv.propEquivBool._proof_1, right_inv := Equiv.propEquivBool._proof_2 }

def Equiv.arrowPUnitEquivPUnit (α : Sort u_1) : (α → PUnit.{v}) ≃ PUnit.{w}

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

Equations

• Equiv.arrowPUnitEquivPUnit α = { toFun := fun (x : α → PUnit.{?u.13}) => PUnit.unit, invFun := fun (x : PUnit.{?u.12}) (x : α) => PUnit.unit, left_inv := ⋯, right_inv := ⋯ }

def Equiv.piUnique {α : Sort u} [Unique α] (β : α → Sort u_1) : ((i : α) → β i) ≃ β default

The equivalence (∀ i, β i) ≃ β ⋆ when the domain of β only contains ⋆

Equations

• Equiv.piUnique β = { toFun := fun (f : (i : α) → β i) => f default, invFun := uniqueElim, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.piUnique_apply {α : Sort u} [Unique α] (β : α → Sort u_1) : ⇑(piUnique β) = fun (f : (i : α) → β i) => f default

@[simp]

theorem Equiv.piUnique_symm_apply {α : Sort u} [Unique α] (β : α → Sort u_1) : ⇑(piUnique β).symm = uniqueElim

def Equiv.funUnique (α : Sort u) (β : Sort u_1) [Unique α] : (α → β) ≃ β

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

Equations

• Equiv.funUnique α β = Equiv.piUnique fun (a : α) => β

@[simp]

theorem Equiv.funUnique_apply (α : Sort u) (β : Sort u_1) [Unique α] : ⇑(funUnique α β) = fun (f : α → β) => f default

@[simp]

theorem Equiv.funUnique_symm_apply (α : Sort u) (β : Sort u_1) [Unique α] : ⇑(funUnique α β).symm = uniqueElim

def Equiv.punitArrowEquiv (α : Sort u_1) : (PUnit.{u} → α) ≃ α

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

Equations

• Equiv.punitArrowEquiv α = Equiv.funUnique PUnit.{?u.9} α

def Equiv.trueArrowEquiv (α : Sort u_1) : (True → α) ≃ α

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

Equations

• Equiv.trueArrowEquiv α = Equiv.funUnique True α

def Equiv.arrowPUnitOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] : (α → β) ≃ PUnit.{u}

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

Equations

• Equiv.arrowPUnitOfIsEmpty α β = { toFun := fun (x : α → β) => PUnit.unit, invFun := fun (x : PUnit.{?u.22}) (a : α) => isEmptyElim a, left_inv := ⋯, right_inv := ⋯ }

def Equiv.emptyArrowEquivPUnit (α : Sort u_1) : (Empty → α) ≃ PUnit.{u}

The sort of maps from Empty is equivalent to PUnit.

Equations

• Equiv.emptyArrowEquivPUnit α = Equiv.arrowPUnitOfIsEmpty Empty α

def Equiv.pemptyArrowEquivPUnit (α : Sort u_1) : (PEmpty.{u_2} → α) ≃ PUnit.{u}

The sort of maps from PEmpty is equivalent to PUnit.

Equations

• Equiv.pemptyArrowEquivPUnit α = Equiv.arrowPUnitOfIsEmpty PEmpty.{?u.8} α

def Equiv.falseArrowEquivPUnit (α : Sort u_1) : (False → α) ≃ PUnit.{u}

The sort of maps from False is equivalent to PUnit.

Equations

• Equiv.falseArrowEquivPUnit α = Equiv.arrowPUnitOfIsEmpty False α

def Equiv.psigmaEquivSigma {α : Type u_2} (β : α → Type u_1) : (i : α) ×' β i ≃ (i : α) × β i

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

Equations

• Equiv.psigmaEquivSigma β = { toFun := fun (a : (i : α) ×' β i) => ⟨a.fst, a.snd⟩, invFun := fun (a : (i : α) × β i) => ⟨a.fst, a.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.psigmaEquivSigma_symm_apply {α : Type u_2} (β : α → Type u_1) (a : (i : α) × β i) : (psigmaEquivSigma β).symm a = ⟨a.fst, a.snd⟩

@[simp]

theorem Equiv.psigmaEquivSigma_apply {α : Type u_2} (β : α → Type u_1) (a : (i : α) ×' β i) : (psigmaEquivSigma β) a = ⟨a.fst, a.snd⟩

def Equiv.psigmaEquivSigmaPLift {α : Sort u_2} (β : α → Sort u_1) : (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.psigmaEquivSigmaPLift_apply {α : Sort u_2} (β : α → Sort u_1) (a : (i : α) ×' β i) : (psigmaEquivSigmaPLift β) a = ⟨{ down := a.fst }, { down := a.snd }⟩

@[simp]

theorem Equiv.psigmaEquivSigmaPLift_symm_apply {α : Sort u_2} (β : α → Sort u_1) (a : (i : PLift α) × PLift (β i.down)) : (psigmaEquivSigmaPLift β).symm a = ⟨a.fst.down, a.snd.down⟩

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 generates an equivalence between Σ' a, β₁ a and Σ' a, β₂ a.

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) : (psigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩

theorem Equiv.psigmaCongrRight_trans {α : Sort u_4} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} {β₃ : α → Sort u_3} (F : (a : α) → β₁ a ≃ β₂ a) (G : (a : α) → β₂ a ≃ β₃ a) : (psigmaCongrRight F).trans (psigmaCongrRight G) = psigmaCongrRight fun (a : α) => (F a).trans (G a)

theorem Equiv.psigmaCongrRight_symm {α : Sort u_3} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (psigmaCongrRight F).symm = psigmaCongrRight fun (a : α) => (F a).symm

@[simp]

theorem Equiv.psigmaCongrRight_refl {α : Sort u_2} {β : α → Sort u_1} : (psigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)

def Equiv.sigmaCongrRight {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type 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.sigmaCongrRight F = { toFun := fun (a : (a : α) × β₁ a) => ⟨a.fst, (F a.fst) a.snd⟩, invFun := fun (a : (a : α) × β₂ a) => ⟨a.fst, (F a.fst).symm a.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sigmaCongrRight_apply {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) (a : (a : α) × β₁ a) : (sigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩

theorem Equiv.sigmaCongrRight_trans {α : Type u_4} {β₁ : α → Type u_1} {β₂ : α → Type u_2} {β₃ : α → Type u_3} (F : (a : α) → β₁ a ≃ β₂ a) (G : (a : α) → β₂ a ≃ β₃ a) : (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun (a : α) => (F a).trans (G a)

theorem Equiv.sigmaCongrRight_symm {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (sigmaCongrRight F).symm = sigmaCongrRight fun (a : α) => (F a).symm

@[simp]

theorem Equiv.sigmaCongrRight_refl {α : Type u_2} {β : α → Type u_1} : (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

• Equiv.psigmaEquivSubtype P = { toFun := fun (x : (i : α) ×' P i) => ⟨x.fst, ⋯⟩, invFun := fun (x : Subtype P) => ⟨↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def Equiv.sigmaPLiftEquivSubtype {α : Type v} (P : α → Prop) : (i : α) × PLift (P i) ≃ Subtype P

A Sigma with PLift fibers is equivalent to the subtype.

Equations

• Equiv.sigmaPLiftEquivSubtype P = ((Equiv.psigmaEquivSigma fun (x : α) => PLift (P x)).symm.trans (Equiv.psigmaCongrRight fun (x : α) => Equiv.plift)).trans (Equiv.psigmaEquivSubtype P)

def Equiv.sigmaULiftPLiftEquivSubtype {α : Type v} (P : α → Prop) : (i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P

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

Equations

• Equiv.sigmaULiftPLiftEquivSubtype P = (Equiv.sigmaCongrRight fun (x : α) => Equiv.ulift).trans (Equiv.sigmaPLiftEquivSubtype P)

@[reducible, inline]

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

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

Equations

• Equiv.Perm.sigmaCongrRight F = Equiv.sigmaCongrRight F

@[simp]

theorem Equiv.Perm.sigmaCongrRight_trans {α : Type u_1} {β : α → Type u_2} (F G : (a : α) → Perm (β a)) : Equiv.trans (sigmaCongrRight F) (sigmaCongrRight G) = sigmaCongrRight fun (a : α) => Equiv.trans (F a) (G a)

@[simp]

theorem Equiv.Perm.sigmaCongrRight_symm {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Perm (β a)) : Equiv.symm (sigmaCongrRight F) = sigmaCongrRight fun (a : α) => Equiv.symm (F a)

@[simp]

theorem Equiv.Perm.sigmaCongrRight_refl {α : Type u_1} {β : α → Type u_2} : (sigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)

def Equiv.functionSwap (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ((a : α) → (b : β) → γ a b) ≃ ((b : β) → (a : α) → γ a b)

Function.swap as an equivalence.

Equations

• Equiv.functionSwap α β γ = { toFun := Function.swap, invFun := Function.swap, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.functionSwap_apply (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ⇑(functionSwap α β γ) = Function.swap

@[simp]

theorem Equiv.functionSwap_symm_apply (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ⇑(functionSwap α β γ).symm = Function.swap

theorem Function.swap_bijective {α : Sort u_1} {β : Sort u_2} {γ : α → β → Sort u_3} : Bijective swap

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

• e.sigmaCongrLeft = { toFun := fun (a : (a : α₁) × β (e a)) => ⟨e a.fst, a.snd⟩, invFun := fun (a : (a : α₂) × β a) => ⟨e.symm a.fst, ⋯ ▸ a.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sigmaCongrLeft_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) (a : (a : α₁) × β (e a)) : e.sigmaCongrLeft a = ⟨e a.fst, a.snd⟩

def Equiv.sigmaCongrLeft' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ → Type u_3} (f : α₁ ≃ α₂) : (a : α₁) × β a ≃ (a : α₂) × β (f.symm a)

Transporting a sigma type through an equivalence of the base

Equations

• f.sigmaCongrLeft' = f.symm.sigmaCongrLeft.symm

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

• f.sigmaCongr F = (Equiv.sigmaCongrRight F).trans f.sigmaCongrLeft

def Equiv.sigmaEquivProd (α : Type u_1) (β : Type u_2) : (_ : α) × β ≃ α × β

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

Equations

• Equiv.sigmaEquivProd α β = { toFun := fun (a : (_ : α) × β) => (a.fst, a.snd), invFun := fun (a : α × β) => ⟨a.fst, a.snd⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sigmaEquivProd_apply (α : Type u_1) (β : Type u_2) (a : (_ : α) × β) : (sigmaEquivProd α β) a = (a.fst, a.snd)

@[simp]

theorem Equiv.sigmaEquivProd_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) : (sigmaEquivProd α β).symm a = ⟨a.fst, a.snd⟩

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

• Equiv.sigmaEquivProdOfEquiv F = (Equiv.sigmaCongrRight F).trans (Equiv.sigmaEquivProd α β)

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

The dependent product of types is associative up to an equivalence.

Equations

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

def Equiv.pSigmaAssoc {α : Sort u_1} {β : α → Sort u_2} (γ : (a : α) → β a → Sort u_3) : (ab : (a : α) ×' β a) ×' γ ab.fst ab.snd ≃ (a : α) ×' (b : β a) ×' γ a b

The dependent product of sorts is associative up to an equivalence.

Equations

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

theorem Equiv.forall_congr_right {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∀ (a : α), q (e a)) ↔ ∀ (b : β), q b

theorem Equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∀ (a : α), p a) ↔ ∀ (b : β), p (e.symm b)

theorem Equiv.forall_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∀ (a : α), p a) ↔ ∀ (b : β), q b

theorem Equiv.forall_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∀ (a : α), p a) ↔ ∀ (b : β), q b

theorem Equiv.exists_congr_right {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∃ (a : α), q (e a)) ↔ ∃ (b : β), q b

theorem Equiv.exists_congr_left {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∃ (a : α), p a) ↔ ∃ (b : β), p (e.symm b)

theorem Equiv.exists_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∃ (a : α), p a) ↔ ∃ (b : β), q b

theorem Equiv.exists_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∃ (a : α), p a) ↔ ∃ (b : β), q b

theorem Equiv.existsUnique_congr_right {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∃! a : α, q (e a)) ↔ ∃! b : β, q b

theorem Equiv.existsUnique_congr_left {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∃! a : α, p a) ↔ ∃! b : β, p (e.symm b)

theorem Equiv.existsUnique_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∃! a : α, p a) ↔ ∃! b : β, q b

theorem Equiv.existsUnique_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∃! a : α, p a) ↔ ∃! b : β, q b

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 (eα x) (eβ 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 (eα.symm x) (eβ.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 (eα x) (eβ y) (eγ 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 (eα.symm x) (eβ.symm y) (eγ.symm z) ↔ q x y z) : (∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z

noncomputable def Equiv.ofBijective {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) : α ≃ β

If f is a bijective function, then its domain is equivalent to its codomain.

Equations

• Equiv.ofBijective f hf = { toFun := f, invFun := Function.surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.ofBijective_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (a✝ : α) : (ofBijective f hf) a✝ = f a✝

theorem Equiv.ofBijective_apply_symm_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : β) : f ((ofBijective f hf).symm x) = x

@[simp]

theorem Equiv.ofBijective_symm_apply_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : α) : (ofBijective f hf).symm (f x) = x

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

• Quot.congr e eq = { toFun := Quot.map ⇑e ⋯, invFun := Quot.map ⇑e.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

@[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) (mk ra a) = mk rb (e a)

def Quot.congrRight {α : Sort u} {r r' : α → α → Prop} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) : Quot r ≃ Quot r'

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

• Quot.congrRight eq = Quot.congr (Equiv.refl α) eq

def Quot.congrLeft {α : Sort u} {β : Sort v} {r : α → α → Prop} (e : α ≃ β) : Quot r ≃ Quot fun (b b' : β) => r (e.symm b) (e.symm 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

• Quot.congrLeft e = Quot.congr e ⋯

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

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

Equations

• Quotient.congr e eq = Quot.congr e eq

@[simp]

theorem Quotient.congr_mk {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) : (Quotient.congr e eq) ⟦a⟧ = ⟦e a⟧

def Quotient.congrRight {α : Sort u} {r r' : Setoid α} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ Quotient r'

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

• Quotient.congrRight eq = Quot.congrRight eq

def finZeroEquiv : Fin 0 ≃ Empty

Equivalence between Fin 0 and Empty.

Equations

• finZeroEquiv = Equiv.equivEmpty (Fin 0)

def finZeroEquiv' : Fin 0 ≃ PEmpty.{u}

Equivalence between Fin 0 and PEmpty.

Equations

• finZeroEquiv' = Equiv.equivPEmpty (Fin 0)

def finOneEquiv : Fin 1 ≃ Unit

Equivalence between Fin 1 and Unit.

Equations

• finOneEquiv = Equiv.equivPUnit (Fin 1)

def finTwoEquiv : Fin 2 ≃ Bool

Equivalence between Fin 2 and Bool.

Equations

• finTwoEquiv = { toFun := fun (i : Fin 2) => i == 1, invFun := fun (b : Bool) => bif b then 1 else 0, left_inv := finTwoEquiv._proof_2, right_inv := finTwoEquiv._proof_3 }

def Equiv.sumIsLeft {α : Type u_1} {β : Type u_2} : { x : α ⊕ β // x.isLeft = true } ≃ α

The left summand of α ⊕ β is equivalent to α.

Equations

• Equiv.sumIsLeft = { toFun := fun (x : { x : α ⊕ β // x.isLeft = true }) => (↑x).getLeft ⋯, invFun := fun (a : α) => ⟨Sum.inl a, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sumIsLeft_apply {α : Type u_1} {β : Type u_2} (x : { x : α ⊕ β // x.isLeft = true }) : sumIsLeft x = (↑x).getLeft ⋯

@[simp]

theorem Equiv.sumIsLeft_symm_apply_coe {α : Type u_1} {β : Type u_2} (a : α) : ↑(sumIsLeft.symm a) = Sum.inl a

def Equiv.sumIsRight {α : Type u_1} {β : Type u_2} : { x : α ⊕ β // x.isRight = true } ≃ β

The right summand of α ⊕ β is equivalent to β.

Equations

• Equiv.sumIsRight = { toFun := fun (x : { x : α ⊕ β // x.isRight = true }) => (↑x).getRight ⋯, invFun := fun (b : β) => ⟨Sum.inr b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.sumIsRight_apply {α : Type u_1} {β : Type u_2} (x : { x : α ⊕ β // x.isRight = true }) : sumIsRight x = (↑x).getRight ⋯

@[simp]

theorem Equiv.sumIsRight_symm_apply_coe {α : Type u_1} {β : Type u_2} (b : β) : ↑(sumIsRight.symm b) = Sum.inr b