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 GroupTheory.Perm.

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., Data.Equiv.TransferInstance does it for many algebraic type classes like Group, Module, etc.

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

Tags

equivalence, congruence, bijective map

ink

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

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

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

ink

def «term_≃_» : Lean.TrailingParserDescr

Equations

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

ink

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.

ink

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 }

ink

def Equiv.Perm (α : Sort u_1) : Sort (max1u_1)

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

Equations

• Equiv.Perm α = (α ≃ α)

ink

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

Equations

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

ink

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

ink

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

ink

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.

ink

theorem Equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ : α ≃ β} {e₂ : α ≃ β} : ↑e₁ = ↑e₂ ↔ e₁ = e₂

ink

theorem Equiv.ext {α : Sort u} {β : Sort v} {f : α ≃ β} {g : α ≃ β} (H : ∀ (x : α), ↑f x = ↑g x) : f = g

ink

theorem Equiv.congr_arg {α : Sort u} {β : Sort v} {f : α ≃ β} {x : α} {x' : α} : x = x' → ↑f x = ↑f x'

ink

theorem Equiv.congr_fun {α : Sort u} {β : Sort v} {f : α ≃ β} {g : α ≃ β} (h : f = g) (x : α) : ↑f x = ↑g x

ink

theorem Equiv.ext_iff {α : Sort u} {β : Sort v} {f : α ≃ β} {g : α ≃ β} : f = g ↔ ∀ (x : α), ↑f x = ↑g x

ink

theorem Equiv.Perm.ext {α : Sort u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (H : ∀ (x : α), ↑σ x = ↑τ x) : σ = τ

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

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

ink

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

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

Equations

• Equiv.symm e = { toFun := e.invFun, invFun := e.toFun, left_inv := (_ : Function.RightInverse e.invFun e.toFun), right_inv := (_ : Function.LeftInverse e.invFun e.toFun) }

ink

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

See Note [custom simps projection]

Equations

• Equiv.Simps.symm_apply e = ↑(Equiv.symm e)

ink

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

ink

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

ink

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.

ink

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

ink

instance Equiv.instTransSortSortSortEquivEquivEquiv : Trans Equiv Equiv Equiv

Equations

• Equiv.instTransSortSortSortEquivEquivEquiv = { trans := fun {a} {b} {c} => Equiv.trans }

ink

@[simp]

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

ink

@[simp]

theorem Equiv.toFun_as_coe_apply {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α) : Equiv.toFun e x = ↑e x

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

• @Equiv.equiv_subsingleton_cod = @Equiv.equiv_subsingleton_cod.proof_1

ink

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

Equations

• @Equiv.equiv_subsingleton_dom = @Equiv.equiv_subsingleton_dom.proof_1

ink

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

Equations

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

ink

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

ink

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

Transfer DecidableEq across an equivalence.

Equations

• Equiv.decidableEq e = Function.Injective.decidableEq (_ : Function.Injective ↑e)

ink

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

ink

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

ink

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

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

Equations

• Equiv.inhabited e = { default := ↑(Equiv.symm e) default }

ink

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

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

Equations

• Equiv.unique e = Function.Surjective.unique ↑(Equiv.symm e) (_ : Function.Surjective ↑(Equiv.symm e))

ink

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

Equivalence between equal types.

Equations

• Equiv.cast h = { toFun := cast h, invFun := cast (_ : β = α), left_inv := (_ : ∀ (x : α), cast (_ : β = α) (cast h x) = x), right_inv := (_ : ∀ (x : β), cast h (cast (_ : β = α) x) = x) }

ink

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

ink

@[simp]

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

ink

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.

ink

@[simp]

theorem Equiv.refl_apply {α : Sort u} (x : α) : ↑(Equiv.refl α) x = x

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

theorem Equiv.symm_symm_apply {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α) : ↑(Equiv.symm (Equiv.symm f)) b = ↑f b

ink

theorem Equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α ≃ β) {x : α} {y : α} : ↑f x = ↑f y ↔ x = y

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

Equations

• Equiv.permCongr e = Equiv.equivCongr e e

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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.

ink

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

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

Equations

• Equiv.equivEmpty α = Equiv.equivOfIsEmpty α Empty

ink

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

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

Equations

• Equiv.equivPEmpty α = Equiv.equivOfIsEmpty α PEmpty

ink

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

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

Equations

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

ink

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

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

Equations

• Equiv.propEquivPEmpty h = Equiv.equivPEmpty p

ink

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.

ink

def Equiv.equivPUnit (α : Sort u) [inst : Unique α] : α ≃ PUnit

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

Equations

• Equiv.equivPUnit α = Equiv.equivOfUnique α PUnit

ink

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

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

Equations

• Equiv.propEquivPUnit h = Equiv.equivPUnit p

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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.

ink

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

ink

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.

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

• Equiv.conj e = Equiv.arrowCongr e e

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

def Equiv.punitEquivPUnit : PUnit ≃ PUnit

PUnit sorts in any two universes are equivalent.

Equations

• Equiv.punitEquivPUnit = { toFun := fun x => PUnit.unit, invFun := fun x => PUnit.unit, left_inv := Equiv.punitEquivPUnit.proof_1, right_inv := Equiv.punitEquivPUnit.proof_2 }

ink

noncomputable def Equiv.propEquivBool : Prop ≃ Bool

Prop is noncomputably equivalent to Bool.

Equations

• Equiv.propEquivBool = { toFun := fun p => decide p, invFun := fun b => b = true, left_inv := Equiv.propEquivBool.proof_1, right_inv := Equiv.propEquivBool.proof_2 }

ink

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.

ink

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

ink

@[simp]

theorem Equiv.piSubsingleton_apply {α : Sort u} (β : α → Sort u_1) [inst : Subsingleton α] (a : α) (f : (x : α) → β x) : ↑(Equiv.piSubsingleton β a) f = Function.eval a f

ink

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.

ink

@[simp]

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

ink

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

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

Equations

• Equiv.funUnique α β = Equiv.piSubsingleton (fun a => β) default

ink

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

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

Equations

• Equiv.punitArrowEquiv α = Equiv.funUnique PUnit α

ink

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

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

Equations

• Equiv.trueArrowEquiv α = Equiv.funUnique True α

ink

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.

ink

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

The sort of maps from Empty is equivalent to PUnit.

Equations

• Equiv.emptyArrowEquivPUnit α = Equiv.arrowPUnitOfIsEmpty Empty α

ink

def Equiv.pemptyArrowEquivPUnit (α : Sort u_1) : (PEmpty → α) ≃ PUnit

The sort of maps from PEmpty is equivalent to PUnit.

Equations

• Equiv.pemptyArrowEquivPUnit α = Equiv.arrowPUnitOfIsEmpty PEmpty α

ink

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

The sort of maps from False is equivalent to PUnit.

Equations

• Equiv.falseArrowEquivPUnit α = Equiv.arrowPUnitOfIsEmpty False α

ink

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

ink

@[simp]

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

ink

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.

ink

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

ink

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

ink

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.

ink

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

ink

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.

ink

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

ink

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

ink

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

ink

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

ink

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.

ink

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

ink

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

ink

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

ink

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.

ink

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.

ink

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

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

ink

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

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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.

ink

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

• Equiv.sigmaCongrLeft' f = Equiv.symm (Equiv.sigmaCongrLeft (Equiv.symm f))

ink

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

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

ink

@[simp]

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

ink

@[simp]

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

ink

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.

ink

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.trans (Equiv.sigmaCongrRight F) (Equiv.sigmaEquivProd α β)

ink

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

Dependent product of types is associative up to an equivalence.

Equations

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

ink

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

ink

theorem Equiv.exists_unique_congr_left' {α : Sort u} {β : Sort v} {p : α → Prop} (f : α ≃ β) : (∃! x, p x) ↔ ∃! y, p (↑(Equiv.symm f) y)

ink

theorem Equiv.exists_unique_congr_left {α : Sort u} {β : Sort v} {p : β → Prop} (f : α ≃ β) : (∃! x, p (↑f x)) ↔ ∃! y, p y

ink

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

ink

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

ink

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

ink

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 eα) x) (↑(Equiv.symm eβ) y) ↔ q x y) : ((x : α₁) → (y : β₁) → p x y) ↔ (x : α₂) → (y : β₂) → q x y

ink

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

ink

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

ink

theorem Equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : α → Prop} (f : α ≃ β) : ((x : α) → p x) ↔ (y : β) → p (↑(Equiv.symm f) y)

ink

theorem Equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : β → Prop} (f : α ≃ β) : ((x : α) → p (↑f x)) ↔ (y : β) → p y

ink

theorem Equiv.exists_congr_left {α : Sort u_1} {β : Sort u_2} (f : α ≃ β) {p : α → Prop} : (∃ a, p a) ↔ ∃ b, p (↑(Equiv.symm f) b)

ink

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.

ink

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

ink

def Quot.congrRight {α : Sort u} {r : α → α → Prop} {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

ink

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

• Quot.congrLeft e = Quot.congr e (_ : ∀ (x x_1 : α), r x x_1 ↔ r (↑(Equiv.symm e) (↑e x)) (↑(Equiv.symm e) (↑e x_1)))

ink

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

ink

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

ink

def Quotient.congrRight {α : Sort u} {r : Setoid α} {r' : Setoid α} (eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ ↔ Setoid.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