logic.equiv.defs - scilib docs

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

source

theorem equiv.refl_apply {α : Sort u} (x : α) :

⇑(equiv.refl α) x = x

source

@[simp]

theorem equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) :

⇑(f.trans g) = ⇑g ∘ ⇑f

source

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

⇑(f.trans g) a = ⇑g (⇑f a)

source

@[simp]

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

⇑e (⇑(e.symm) x) = x

source

@[simp]

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

⇑(e.symm) (⇑e x) = x

source

@[simp]

theorem equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α ≃ β) :

⇑(e.symm) ∘ ⇑e = id

source

@[simp]

theorem equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α ≃ β) :

⇑e ∘ ⇑(e.symm) = id

source

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

source

@[simp, nolint]

theorem equiv.symm_symm_apply {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α) :

⇑(f.symm.symm) b = ⇑f b

source

theorem equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α} :

⇑f x = ⇑f y ↔ x = y

source

theorem equiv.apply_eq_iff_eq_symm_apply {α : Sort u_1} {β : Sort u_2} (f : α ≃ β) {x : α} {y : β} :

⇑f x = y ↔ x = ⇑(f.symm) y

source

@[simp]

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

⇑(equiv.cast h) x = cast h x

source

@[simp]

theorem equiv.cast_symm {α β : Sort u_1} (h : α = β) :

(equiv.cast h).symm = equiv.cast _

source

@[simp]

theorem equiv.cast_refl {α : Sort u_1} (h : α = α := rfl) :

equiv.cast h = equiv.refl α

source

@[simp]

theorem equiv.cast_trans {α β γ : Sort u_1} (h : α = β) (h2 : β = γ) :

(equiv.cast h).trans (equiv.cast h2) = equiv.cast _

source

theorem equiv.cast_eq_iff_heq {α β : Sort u_1} (h : α = β) {a : α} {b : β} :

⇑(equiv.cast h) a = b ↔ a == b

source

theorem equiv.symm_apply_eq {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} :

⇑(e.symm) x = y ↔ x = ⇑e y

source

theorem equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} :

y = ⇑(e.symm) x ↔ ⇑e y = x

source

@[simp]

theorem equiv.symm_symm {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.symm.symm = e

source

@[simp]

theorem equiv.trans_refl {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.trans (equiv.refl β) = e

source

@[simp]

theorem equiv.refl_symm {α : Sort u} :

(equiv.refl α).symm = equiv.refl α

source

@[simp]

theorem equiv.refl_trans {α : Sort u} {β : Sort v} (e : α ≃ β) :

(equiv.refl α).trans e = e

source

@[simp]

theorem equiv.symm_trans_self {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.symm.trans e = equiv.refl β

source

@[simp]

theorem equiv.self_trans_symm {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.trans e.symm = equiv.refl α

source

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)

source

theorem equiv.left_inverse_symm {α : Sort u} {β : Sort v} (f : α ≃ β) :

function.left_inverse ⇑(f.symm) ⇑f

source

theorem equiv.right_inverse_symm {α : Sort u} {β : Sort v} (f : α ≃ β) :

function.right_inverse ⇑(f.symm) ⇑f

source

theorem equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) :

function.injective (f ∘ ⇑e) ↔ function.injective f

source

theorem equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) :

function.injective (⇑e ∘ f) ↔ function.injective f

source

theorem equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) :

function.surjective (f ∘ ⇑e) ↔ function.surjective f

source

theorem equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) :

function.surjective (⇑e ∘ f) ↔ function.surjective f

source

theorem equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) :

function.bijective (f ∘ ⇑e) ↔ function.bijective f

source

theorem equiv.comp_bijective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) :

function.bijective (⇑e ∘ f) ↔ function.bijective f

source

def equiv.equiv_congr {α : 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.equiv_congr cd = {to_fun := λ (ac : α ≃ γ), (ab.symm.trans ac).trans cd, inv_fun := λ (bd : β ≃ δ), ab.trans (bd.trans cd.symm), left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.equiv_congr_refl {α : Sort u_1} {β : Sort u_2} :

(equiv.refl α).equiv_congr (equiv.refl β) = equiv.refl (α ≃ β)

source

@[simp]

theorem equiv.equiv_congr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) :

(ab.equiv_congr cd).symm = ab.symm.equiv_congr cd.symm

source

@[simp]

theorem equiv.equiv_congr_trans {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α ≃ β) (de : δ ≃ ε) (bc : β ≃ γ) (ef : ε ≃ ζ) :

(ab.equiv_congr de).trans (bc.equiv_congr ef) = (ab.trans bc).equiv_congr (de.trans ef)

source

@[simp]

theorem equiv.equiv_congr_refl_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β ≃ γ) (e : α ≃ β) :

⇑((equiv.refl α).equiv_congr bg) e = e.trans bg

source

@[simp]

theorem equiv.equiv_congr_refl_right {α : Sort u_1} {β : Sort u_2} (ab e : α ≃ β) :

⇑(ab.equiv_congr (equiv.refl β)) e = ab.symm.trans e

source

@[simp]

theorem equiv.equiv_congr_apply_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) (e : α ≃ γ) (x : β) :

⇑(⇑(ab.equiv_congr cd) e) x = ⇑cd (⇑e (⇑(ab.symm) x))

source

def equiv.perm_congr {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') :

equiv.perm α' ≃ equiv.perm β'

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

Equations

e.perm_congr = e.equiv_congr e

source

theorem equiv.perm_congr_def {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : equiv.perm α') :

⇑(e.perm_congr) p = (e.symm.trans p).trans e

source

@[simp]

theorem equiv.perm_congr_refl {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') :

⇑(e.perm_congr) (equiv.refl α') = equiv.refl β'

source

@[simp]

theorem equiv.perm_congr_symm {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') :

e.perm_congr.symm = e.symm.perm_congr

source

@[simp]

theorem equiv.perm_congr_apply {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : equiv.perm α') (x : β') :

⇑(⇑(e.perm_congr) p) x = ⇑e (⇑p (⇑(e.symm) x))

source

theorem equiv.perm_congr_symm_apply {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : equiv.perm β') (x : α') :

⇑(⇑(e.perm_congr.symm) p) x = ⇑(e.symm) (⇑p (⇑e x))

source

theorem equiv.perm_congr_trans {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p p' : equiv.perm α') :

equiv.trans (⇑(e.perm_congr) p) (⇑(e.perm_congr) p') = ⇑(e.perm_congr) (equiv.trans p p')

source

def equiv.equiv_of_is_empty (α : Sort u_1) (β : Sort u_2) [is_empty α] [is_empty β] :

α ≃ β

Two empty types are equivalent.

Equations

equiv.equiv_of_is_empty α β = {to_fun := is_empty_elim (λ (a : α), β), inv_fun := is_empty_elim (λ (a : β), α), left_inv := _, right_inv := _}

source

def equiv.equiv_empty (α : Sort u) [is_empty α] :

α ≃ empty

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

Equations

equiv.equiv_empty α = equiv.equiv_of_is_empty α empty

source

def equiv.equiv_pempty (α : Sort v) [is_empty α] :

α ≃ pempty

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

Equations

equiv.equiv_pempty α = equiv.equiv_of_is_empty α pempty

source

def equiv.equiv_empty_equiv (α : Sort u) :

α ≃ empty ≃ is_empty α

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

Equations

equiv.equiv_empty_equiv α = {to_fun := _, inv_fun := equiv.equiv_empty α, left_inv := _, right_inv := _}

source

def equiv.prop_equiv_pempty {p : Prop} (h : ¬p) :

p ≃ pempty

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

Equations

equiv.prop_equiv_pempty h = equiv.equiv_pempty p

source

def equiv.equiv_of_unique (α : Sort u_1) (β : Sort u_2) [unique α] [unique β] :

α ≃ β

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

Equations

equiv.equiv_of_unique α β = {to_fun := inhabited.default (pi.inhabited α), inv_fun := inhabited.default (pi.inhabited β), left_inv := _, right_inv := _}

source

def equiv.equiv_punit (α : Sort u_1) [unique α] :

α ≃ punit

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

Equations

equiv.equiv_punit α = equiv.equiv_of_unique α punit

source

def equiv.prop_equiv_punit {p : Prop} (h : p) :

p ≃ punit

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

Equations

equiv.prop_equiv_punit h = equiv.equiv_punit p

source

@[simp]

theorem equiv.ulift_symm_apply {α : Type v} :

⇑(equiv.ulift.symm) = ulift.up

source

@[protected]

def equiv.ulift {α : Type v} :

ulift α ≃ α

ulift α is equivalent to α.

Equations

equiv.ulift = {to_fun := ulift.down α, inv_fun := ulift.up α, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.ulift_apply {α : Type v} :

⇑equiv.ulift = ulift.down

source

@[simp]

theorem equiv.plift_apply {α : Sort u} :

⇑equiv.plift = plift.down

source

@[protected]

def equiv.plift {α : Sort u} :

plift α ≃ α

plift α is equivalent to α.

Equations

equiv.plift = {to_fun := plift.down α, inv_fun := plift.up α, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.plift_symm_apply {α : Sort u} :

⇑(equiv.plift.symm) = plift.up

source

def equiv.of_iff {P Q : Prop} (h : P ↔ Q) :

P ≃ Q

equivalence of propositions is the same as iff

Equations

equiv.of_iff h = {to_fun := _, inv_fun := _, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.arrow_congr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) (ᾰ : α₂) :

⇑(e₁.arrow_congr e₂) f ᾰ = (⇑e₂ ∘ f ∘ ⇑(e₁.symm)) ᾰ

source

def equiv.arrow_congr {α₁ : 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₁.arrow_congr e₂ = {to_fun := λ (f : α₁ → β₁), ⇑e₂ ∘ f ∘ ⇑(e₁.symm), inv_fun := λ (f : α₂ → β₂), ⇑(e₂.symm) ∘ f ∘ ⇑e₁, left_inv := _, right_inv := _}

source

theorem equiv.arrow_congr_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.arrow_congr ec) (g ∘ f) = ⇑(eb.arrow_congr ec) g ∘ ⇑(ea.arrow_congr eb) f

source

@[simp]

theorem equiv.arrow_congr_refl {α : Sort u_1} {β : Sort u_2} :

(equiv.refl α).arrow_congr (equiv.refl β) = equiv.refl (α → β)

source

@[simp]

theorem equiv.arrow_congr_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₂).arrow_congr (e₁'.trans e₂') = (e₁.arrow_congr e₁').trans (e₂.arrow_congr e₂')

source

@[simp]

theorem equiv.arrow_congr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :

(e₁.arrow_congr e₂).symm = e₁.symm.arrow_congr e₂.symm

source

def equiv.arrow_congr' {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) :

(α₁ → β₁) ≃ (α₂ → β₂)

A version of equiv.arrow_congr in Type, rather than Sort.

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

Equations

hα.arrow_congr' hβ = hα.arrow_congr hβ

source

@[simp]

theorem equiv.arrow_congr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) (f : α₁ → β₁) (ᾰ : α₂) :

⇑(hα.arrow_congr' hβ) f ᾰ = ⇑hβ (f (⇑(hα.symm) ᾰ))

source

@[simp]

theorem equiv.arrow_congr'_refl {α : Type u_1} {β : Type u_2} :

(equiv.refl α).arrow_congr' (equiv.refl β) = equiv.refl (α → β)

source

@[simp]

theorem equiv.arrow_congr'_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₂).arrow_congr' (e₁'.trans e₂') = (e₁.arrow_congr' e₁').trans (e₂.arrow_congr' e₂')

source

@[simp]

theorem equiv.arrow_congr'_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :

(e₁.arrow_congr' e₂).symm = e₁.symm.arrow_congr' e₂.symm

source

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

(α → α) ≃ (β → β)

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

Equations

e.conj = e.arrow_congr e

source

@[simp]

theorem equiv.conj_apply {α : Sort u} {β : Sort v} (e : α ≃ β) (f : α → α) (ᾰ : β) :

⇑(e.conj) f ᾰ = ⇑e (f (⇑(e.symm) ᾰ))

source

@[simp]

theorem equiv.conj_refl {α : Sort u} :

(equiv.refl α).conj = equiv.refl (α → α)

source

@[simp]

theorem equiv.conj_symm {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.conj.symm = e.symm.conj

source

@[simp]

theorem equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) :

(e₁.trans e₂).conj = e₁.conj.trans e₂.conj

source

theorem equiv.conj_comp {α : Sort u} {β : Sort v} (e : α ≃ β) (f₁ f₂ : α → α) :

⇑(e.conj) (f₁ ∘ f₂) = ⇑(e.conj) f₁ ∘ ⇑(e.conj) f₂

source

theorem equiv.eq_comp_symm {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ) :

f = g ∘ ⇑(e.symm) ↔ f ∘ ⇑e = g

source

theorem equiv.comp_symm_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ) :

g ∘ ⇑(e.symm) = f ↔ g = f ∘ ⇑e

source

theorem equiv.eq_symm_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β) :

f = ⇑(e.symm) ∘ g ↔ ⇑e ∘ f = g

source

theorem equiv.symm_comp_eq {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β) :

⇑(e.symm) ∘ g = f ↔ g = ⇑e ∘ f

source

def equiv.punit_equiv_punit :

punit ≃ punit

punit sorts in any two universes are equivalent.

Equations

equiv.punit_equiv_punit = {to_fun := λ (_x : punit), punit.star, inv_fun := λ (_x : punit), punit.star, left_inv := equiv.punit_equiv_punit._proof_1, right_inv := equiv.punit_equiv_punit._proof_2}

source

noncomputable def equiv.Prop_equiv_bool :

Prop ≃ bool

Prop is noncomputably equivalent to bool.

Equations

equiv.Prop_equiv_bool = {to_fun := λ (p : Prop), decidable.to_bool p, inv_fun := λ (b : bool), ↥b, left_inv := equiv.Prop_equiv_bool._proof_1, right_inv := equiv.Prop_equiv_bool._proof_2}

source

def equiv.arrow_punit_equiv_punit (α : Sort u_1) :

(α → punit) ≃ punit

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

Equations

equiv.arrow_punit_equiv_punit α = {to_fun := λ (f : α → punit), punit.star, inv_fun := λ (u : punit) (f : α), punit.star, left_inv := _, right_inv := _}

source

def equiv.Pi_subsingleton {α : Sort u_1} (β : α → Sort u_2) [subsingleton α] (a : α) :

(Π (a' : α), β a') ≃ β a

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

Equations

equiv.Pi_subsingleton β a = {to_fun := function.eval a, inv_fun := λ (x : β a) (b : α), cast _ x, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.Pi_subsingleton_symm_apply {α : Sort u_1} (β : α → Sort u_2) [subsingleton α] (a : α) (x : β a) (b : α) :

⇑((equiv.Pi_subsingleton β a).symm) x b = cast _ x

source

@[simp]

theorem equiv.Pi_subsingleton_apply {α : Sort u_1} (β : α → Sort u_2) [subsingleton α] (a : α) (f : Π (x : α), (λ (a' : α), β a') x) :

⇑(equiv.Pi_subsingleton β a) f = function.eval a f

source

def equiv.fun_unique (α : Sort u_1) (β : Sort u_2) [unique α] :

(α → β) ≃ β

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

Equations

equiv.fun_unique α β = equiv.Pi_subsingleton (λ (ᾰ : α), β) inhabited.default

source

@[simp]

theorem equiv.fun_unique_symm_apply (α : Sort u_1) (β : Sort u_2) [unique α] :

⇑((equiv.fun_unique α β).symm) = λ (x : β) (b : α), x

source

@[simp]

theorem equiv.fun_unique_apply (α : Sort u_1) (β : Sort u_2) [unique α] :

⇑(equiv.fun_unique α β) = function.eval inhabited.default

source

def equiv.punit_arrow_equiv (α : Sort u_1) :

(punit → α) ≃ α

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

Equations

equiv.punit_arrow_equiv α = equiv.fun_unique punit α

source

def equiv.true_arrow_equiv (α : Sort u_1) :

(true → α) ≃ α

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

Equations

equiv.true_arrow_equiv α = equiv.fun_unique true α

source

def equiv.arrow_punit_of_is_empty (α : Sort u_1) (β : Sort u_2) [is_empty α] :

(α → β) ≃ punit

The sort of maps from a type that is_empty is equivalent to punit.

Equations

equiv.arrow_punit_of_is_empty α β = {to_fun := λ (f : α → β), punit.star, inv_fun := λ (u : punit), is_empty_elim, left_inv := _, right_inv := _}

source

def equiv.empty_arrow_equiv_punit (α : Sort u_1) :

(empty → α) ≃ punit

The sort of maps from empty is equivalent to punit.

Equations

equiv.empty_arrow_equiv_punit α = equiv.arrow_punit_of_is_empty empty α

source

def equiv.pempty_arrow_equiv_punit (α : Sort u_1) :

(pempty → α) ≃ punit

The sort of maps from pempty is equivalent to punit.

Equations

equiv.pempty_arrow_equiv_punit α = equiv.arrow_punit_of_is_empty pempty α

source

def equiv.false_arrow_equiv_punit (α : Sort u_1) :

(false → α) ≃ punit

The sort of maps from false is equivalent to punit.

Equations

equiv.false_arrow_equiv_punit α = equiv.arrow_punit_of_is_empty false α

source

def equiv.psigma_equiv_sigma {α : Type u_1} (β : α → Type u_2) :

(Σ' (i : α), β i) ≃ Σ (i : α), β i

A psigma-type is equivalent to the corresponding sigma-type.

Equations

equiv.psigma_equiv_sigma β = {to_fun := λ (a : Σ' (i : α), β i), ⟨a.fst, a.snd⟩, inv_fun := λ (a : Σ (i : α), β i), ⟨a.fst, a.snd⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.psigma_equiv_sigma_symm_apply {α : Type u_1} (β : α → Type u_2) (a : Σ (i : α), β i) :

⇑((equiv.psigma_equiv_sigma β).symm) a = ⟨a.fst, a.snd⟩

source

@[simp]

theorem equiv.psigma_equiv_sigma_apply {α : Type u_1} (β : α → Type u_2) (a : Σ' (i : α), β i) :

⇑(equiv.psigma_equiv_sigma β) a = ⟨a.fst, a.snd⟩

source

def equiv.psigma_equiv_sigma_plift {α : Sort u_1} (β : α → Sort u_2) :

(Σ' (i : α), β i) ≃ Σ (i : plift α), plift (β i.down)

A psigma-type is equivalent to the corresponding sigma-type.

Equations

equiv.psigma_equiv_sigma_plift β = {to_fun := λ (a : Σ' (i : α), β i), ⟨{down := a.fst}, {down := a.snd}⟩, inv_fun := λ (a : Σ (i : plift α), plift (β i.down)), ⟨a.fst.down, a.snd.down⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.psigma_equiv_sigma_plift_apply {α : Sort u_1} (β : α → Sort u_2) (a : Σ' (i : α), β i) :

⇑(equiv.psigma_equiv_sigma_plift β) a = ⟨{down := a.fst}, {down := a.snd}⟩

source

@[simp]

theorem equiv.psigma_equiv_sigma_plift_symm_apply {α : Sort u_1} (β : α → Sort u_2) (a : Σ (i : plift α), plift (β i.down)) :

⇑((equiv.psigma_equiv_sigma_plift β).symm) a = ⟨a.fst.down, a.snd.down⟩

source

@[simp]

theorem equiv.psigma_congr_right_apply {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (F : Π (a : α), β₁ a ≃ β₂ a) (a : Σ' (a : α), β₁ a) :

⇑(equiv.psigma_congr_right F) a = ⟨a.fst, ⇑(F a.fst) a.snd⟩

source

def equiv.psigma_congr_right {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (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.psigma_congr_right F = {to_fun := λ (a : Σ' (a : α), β₁ a), ⟨a.fst, ⇑(F a.fst) a.snd⟩, inv_fun := λ (a : Σ' (a : α), β₂ a), ⟨a.fst, ⇑((F a.fst).symm) a.snd⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.psigma_congr_right_trans {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} {β₃ : α → Sort u_4} (F : Π (a : α), β₁ a ≃ β₂ a) (G : Π (a : α), β₂ a ≃ β₃ a) :

(equiv.psigma_congr_right F).trans (equiv.psigma_congr_right G) = equiv.psigma_congr_right (λ (a : α), (F a).trans (G a))

source

@[simp]

theorem equiv.psigma_congr_right_symm {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (F : Π (a : α), β₁ a ≃ β₂ a) :

(equiv.psigma_congr_right F).symm = equiv.psigma_congr_right (λ (a : α), (F a).symm)

source

@[simp]

theorem equiv.psigma_congr_right_refl {α : Sort u_1} {β : α → Sort u_2} :

equiv.psigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ' (a : α), β a)

source

@[simp]

theorem equiv.sigma_congr_right_apply {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a ≃ β₂ a) (a : Σ (a : α), β₁ a) :

⇑(equiv.sigma_congr_right F) a = ⟨a.fst, ⇑(F a.fst) a.snd⟩

source

def equiv.sigma_congr_right {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (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.sigma_congr_right F = {to_fun := λ (a : Σ (a : α), β₁ a), ⟨a.fst, ⇑(F a.fst) a.snd⟩, inv_fun := λ (a : Σ (a : α), β₂ a), ⟨a.fst, ⇑((F a.fst).symm) a.snd⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sigma_congr_right_trans {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} {β₃ : α → Type u_4} (F : Π (a : α), β₁ a ≃ β₂ a) (G : Π (a : α), β₂ a ≃ β₃ a) :

(equiv.sigma_congr_right F).trans (equiv.sigma_congr_right G) = equiv.sigma_congr_right (λ (a : α), (F a).trans (G a))

source

@[simp]

theorem equiv.sigma_congr_right_symm {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a ≃ β₂ a) :

(equiv.sigma_congr_right F).symm = equiv.sigma_congr_right (λ (a : α), (F a).symm)

source

@[simp]

theorem equiv.sigma_congr_right_refl {α : Type u_1} {β : α → Type u_2} :

equiv.sigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ (a : α), β a)

source

def equiv.psigma_equiv_subtype {α : Type v} (P : α → Prop) :

(Σ' (i : α), P i) ≃ subtype P

A psigma with Prop fibers is equivalent to the subtype.

Equations

equiv.psigma_equiv_subtype P = {to_fun := λ (x : Σ' (i : α), P i), ⟨x.fst, _⟩, inv_fun := λ (x : subtype P), ⟨x.val, _⟩, left_inv := _, right_inv := _}

source

def equiv.sigma_plift_equiv_subtype {α : Type v} (P : α → Prop) :

(Σ (i : α), plift (P i)) ≃ subtype P

A sigma with plift fibers is equivalent to the subtype.

Equations

equiv.sigma_plift_equiv_subtype P = ((equiv.psigma_equiv_sigma (λ (i : α), plift (P i))).symm.trans (equiv.psigma_congr_right (λ (a : α), equiv.plift))).trans (equiv.psigma_equiv_subtype P)

source

def equiv.sigma_ulift_plift_equiv_subtype {α : 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 sigma_plift_equiv_subtype.

Equations

equiv.sigma_ulift_plift_equiv_subtype P = (equiv.sigma_congr_right (λ (a : α), equiv.ulift)).trans (equiv.sigma_plift_equiv_subtype P)

source

@[reducible]

def equiv.perm.sigma_congr_right {α : 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.sigma_congr_right F = equiv.sigma_congr_right F

source

@[simp]

theorem equiv.perm.sigma_congr_right_trans {α : Type u_1} {β : α → Type u_2} (F G : Π (a : α), equiv.perm (β a)) :

equiv.trans (equiv.perm.sigma_congr_right F) (equiv.perm.sigma_congr_right G) = equiv.perm.sigma_congr_right (λ (a : α), equiv.trans (F a) (G a))

source

@[simp]

theorem equiv.perm.sigma_congr_right_symm {α : Type u_1} {β : α → Type u_2} (F : Π (a : α), equiv.perm (β a)) :

equiv.symm (equiv.perm.sigma_congr_right F) = equiv.perm.sigma_congr_right (λ (a : α), equiv.symm (F a))

source

@[simp]

theorem equiv.perm.sigma_congr_right_refl {α : Type u_1} {β : α → Type u_2} :

equiv.perm.sigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ (a : α), β a)

source

@[simp]

theorem equiv.sigma_congr_left_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) (a : Σ (a : α₁), β (⇑e a)) :

⇑(e.sigma_congr_left) a = ⟨⇑e a.fst, a.snd⟩

source

def equiv.sigma_congr_left {α₁ : 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.sigma_congr_left = {to_fun := λ (a : Σ (a : α₁), β (⇑e a)), ⟨⇑e a.fst, a.snd⟩, inv_fun := λ (a : Σ (a : α₂), β a), ⟨⇑(e.symm) a.fst, eq.rec a.snd _⟩, left_inv := _, right_inv := _}

source

def equiv.sigma_congr_left' {α₁ : 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.sigma_congr_left' = f.symm.sigma_congr_left.symm

source

def equiv.sigma_congr {α₁ : 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.sigma_congr F = (equiv.sigma_congr_right F).trans f.sigma_congr_left

source

def equiv.sigma_equiv_prod (α : Type u_1) (β : Type u_2) :

(Σ (_x : α), β) ≃ α × β

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

Equations

equiv.sigma_equiv_prod α β = {to_fun := λ (a : Σ (_x : α), β), (a.fst, a.snd), inv_fun := λ (a : α × β), ⟨a.fst, a.snd⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sigma_equiv_prod_apply (α : Type u_1) (β : Type u_2) (a : Σ (_x : α), β) :

⇑(equiv.sigma_equiv_prod α β) a = (a.fst, a.snd)

source

@[simp]

theorem equiv.sigma_equiv_prod_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :

⇑((equiv.sigma_equiv_prod α β).symm) a = ⟨a.fst, a.snd⟩

source

def equiv.sigma_equiv_prod_of_equiv {α : 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.sigma_equiv_prod_of_equiv F = (equiv.sigma_congr_right F).trans (equiv.sigma_equiv_prod α β)

source

def equiv.sigma_assoc {α : 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

equiv.sigma_assoc γ = {to_fun := λ (x : Σ (ab : Σ (a : α), β a), γ ab.fst ab.snd), ⟨x.fst.fst, ⟨x.fst.snd, x.snd⟩⟩, inv_fun := λ (x : Σ (a : α) (b : β a), γ a b), ⟨⟨x.fst, x.snd.fst⟩, x.snd.snd⟩, left_inv := _, right_inv := _}

source

@[protected]

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

source

@[protected]

theorem equiv.exists_unique_congr_left' {α : Sort u} {β : Sort v} {p : α → Prop} (f : α ≃ β) :

(∃! (x : α), p x) ↔ ∃! (y : β), p (⇑(f.symm) y)

source

@[protected]

theorem equiv.exists_unique_congr_left {α : Sort u} {β : Sort v} {p : β → Prop} (f : α ≃ β) :

(∃! (x : α), p (⇑f x)) ↔ ∃! (y : β), p y

source

@[protected]

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

source

@[protected]

theorem equiv.forall_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (f : α ≃ β) (h : ∀ {x : β}, p (⇑(f.symm) x) ↔ q x) :

(∀ (x : α), p x) ↔ ∀ (y : β), q y

source

@[protected]

theorem equiv.forall₂_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {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

source

@[protected]

theorem equiv.forall₂_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {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

source

@[protected]

theorem equiv.forall₃_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {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

source

@[protected]

theorem equiv.forall₃_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {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

source

@[protected]

theorem equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : α → Prop} (f : α ≃ β) :

(∀ (x : α), p x) ↔ ∀ (y : β), p (⇑(f.symm) y)

source

@[protected]

theorem equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : β → Prop} (f : α ≃ β) :

(∀ (x : α), p (⇑f x)) ↔ ∀ (y : β), p y

source

@[protected]

theorem equiv.exists_congr_left {α : Sort u_1} {β : Sort u_2} (f : α ≃ β) {p : α → Prop} :

(∃ (a : α), p a) ↔ ∃ (b : β), p (⇑(f.symm) b)

source

@[protected]

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 = {to_fun := quot.map ⇑e _, inv_fun := quot.map ⇑(e.symm) _, left_inv := _, right_inv := _}

source

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

source

@[protected]

def quot.congr_right {α : 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.congr_right eq = quot.congr (equiv.refl α) eq

source

@[protected]

def quot.congr_left {α : Sort u} {β : Sort v} {r : α → α → Prop} (e : α ≃ β) :

quot r ≃ quot (λ (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.congr_left e = quot.congr e _

source

@[protected]

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

source

@[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) ⟦a⟧ = ⟦⇑e a⟧

source

@[protected]

def quotient.congr_right {α : Sort u} {r 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.congr_right eq = quot.congr_right eq

scilib documentation

Equivalence between types #

Tags #