mathlib documentation

data.equiv.basic

Equivalence between types #

In this file we define two types:

Then we define

Tags #

equivalence, congruence, bijective map

source
@[nolint]
structure equiv (α : Sort u_1) (β : Sort u_2) :
Sort (max 1 (imax u_1 u_2) (imax u_2 u_1))

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

source
def function.involutive.to_equiv {α : Sort u} (f : α → α) (h : function.involutive f) :
α ≃ α

Convert an involutive function f to an equivalence with to_fun = inv_fun = f.

Equations
source
def equiv.perm (α : Sort u_1) :
Sort (max 1 u_1)

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

Equations
source
@[protected, instance]
def equiv.has_coe_to_fun {α : Sort u} {β : Sort v} :
has_coe_to_fun (α ≃ β) (λ (_x : α ≃ β), α → β)
Equations
source
@[simp]
theorem equiv.coe_fn_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : function.left_inverse g f) (r : function.right_inverse g f) :
⇑{to_fun := f, inv_fun := g, left_inv := l, right_inv := r} = f
source
theorem equiv.coe_fn_injective {α : Sort u} {β : Sort v} :
function.injective coe_fn

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

source
@[protected, simp, norm_cast]
theorem equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β} :
⇑e₁ = ⇑e₂ ↔ e₁ = e₂
source
@[ext]
theorem equiv.ext {α : Sort u} {β : Sort v} {f g : α ≃ β} (H : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
source
@[protected]
theorem equiv.congr_arg {α : Sort u} {β : Sort v} {f : α ≃ β} {x x' : α} :
x = x' → ⇑f x = ⇑f x'
source
@[protected]
theorem equiv.congr_fun {α : Sort u} {β : Sort v} {f g : α ≃ β} (h : f = g) (x : α) :
⇑f x = ⇑g x
source
theorem equiv.ext_iff {α : Sort u} {β : Sort v} {f g : α ≃ β} :
f = g ↔ ∀ (x : α), ⇑f x = ⇑g x
source
@[ext]
theorem equiv.perm.ext {α : Sort u} {σ τ : equiv.perm α} (H : ∀ (x : α), ⇑σ x = ⇑τ x) :
σ = τ
source
@[protected]
theorem equiv.perm.congr_arg {α : Sort u} {f : equiv.perm α} {x x' : α} :
x = x' → ⇑f x = ⇑f x'
source
@[protected]
theorem equiv.perm.congr_fun {α : Sort u} {f g : equiv.perm α} (h : f = g) (x : α) :
⇑f x = ⇑g x
source
theorem equiv.perm.ext_iff {α : Sort u} {σ τ : equiv.perm α} :
σ = τ ↔ ∀ (x : α), ⇑σ x = ⇑τ x
source
@[protected]
def equiv.refl (α : Sort u_1) :
α ≃ α

Any type is equivalent to itself.

Equations
source
@[protected, instance]
def equiv.inhabited' {α : Sort u} :
inhabited (α ≃ α)
Equations
source
@[protected]
def equiv.symm {α : Sort u} {β : Sort v} (e : α ≃ β) :
β ≃ α

Inverse of an equivalence e : α ≃ β.

Equations
source
def equiv.simps.symm_apply {α : Sort u} {β : Sort v} (e : α ≃ β) :
β → α

See Note [custom simps projection]

Equations
source
@[simp]
theorem function.involutive.to_equiv_apply {α : Sort u} (f : α → α) (h : function.involutive f) (ᾰ : α) :
⇑(function.involutive.to_equiv f h) ᾰ = f ᾰ
source
@[simp]
theorem function.involutive.to_equiv_symm_apply {α : Sort u} (f : α → α) (h : function.involutive f) (ᾰ : α) :
⇑((function.involutive.to_equiv f h).symm) ᾰ = f ᾰ
source
@[protected]
def equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) :
α ≃ γ

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

Equations
source
@[simp]
theorem equiv.to_fun_as_coe {α : Sort u} {β : Sort v} (e : α ≃ β) :
e.to_fun = ⇑e
source
@[simp]
theorem equiv.inv_fun_as_coe {α : Sort u} {β : Sort v} (e : α ≃ β) :
e.inv_fun = ⇑(e.symm)
source
@[protected]
theorem equiv.injective {α : Sort u} {β : Sort v} (e : α ≃ β) :
function.injective ⇑e
source
@[protected]
theorem equiv.surjective {α : Sort u} {β : Sort v} (e : α ≃ β) :
function.surjective ⇑e
source
@[protected]
theorem equiv.bijective {α : Sort u} {β : Sort v} (f : α ≃ β) :
function.bijective ⇑f
source
@[protected]
theorem equiv.subsingleton {α : Sort u} {β : Sort v} (e : α ≃ β) [subsingleton β] :
subsingleton α
source
@[protected]
theorem equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α ≃ β) [subsingleton α] :
subsingleton β
source
theorem equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α ≃ β) :
subsingleton α ↔ subsingleton β
source
@[protected, instance]
def equiv.equiv_subsingleton_cod {α : Sort u} {β : Sort v} [subsingleton β] :
subsingleton (α ≃ β)
source
@[protected, instance]
def equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [subsingleton α] :
subsingleton (α ≃ β)
source
@[protected, instance]
def equiv.perm_unique {α : Sort u} [subsingleton α] :
unique (equiv.perm α)
Equations
source
theorem equiv.perm.subsingleton_eq_refl {α : Sort u} [subsingleton α] (e : equiv.perm α) :
e = equiv.refl α
source
@[protected]
def equiv.decidable_eq {α : Sort u} {β : Sort v} (e : α ≃ β) [decidable_eq β] :
decidable_eq α

Transfer decidable_eq across an equivalence.

Equations
source
theorem equiv.nonempty_congr {α : Sort u} {β : Sort v} (e : α ≃ β) :
nonempty α ↔ nonempty β
source
@[protected]
theorem equiv.nonempty {α : Sort u} {β : Sort v} (e : α ≃ β) [nonempty β] :
nonempty α
source
@[protected]
def equiv.inhabited {α : Sort u} {β : Sort v} [inhabited β] (e : α ≃ β) :
inhabited α

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

Equations
source
@[protected]
def equiv.unique {α : Sort u} {β : Sort v} [unique β] (e : α ≃ β) :
unique α

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

Equations
source
@[protected]
def equiv.cast {α β : Sort u_1} (h : α = β) :
α ≃ β

Equivalence between equal types.

Equations
source
@[simp]
theorem equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : function.left_inverse g f) (r : function.right_inverse g f) :
⇑({to_fun := f, inv_fun := g, left_inv := l, right_inv := r}.symm) = g
source
@[simp]
theorem equiv.coe_refl {α : Sort u} :
⇑(equiv.refl α) = id
source
@[simp]
theorem equiv.perm.coe_subsingleton {α : Type u_1} [subsingleton α] (e : equiv.perm α) :
⇑e = id
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
@[simp]
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
@[simp]
theorem equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) :
function.injective (f ∘ ⇑e) ↔ function.injective f
source
@[simp]
theorem equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) :
function.injective (⇑e ∘ f) ↔ function.injective f
source
@[simp]
theorem equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) :
function.surjective (f ∘ ⇑e) ↔ function.surjective f
source
@[simp]
theorem equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) :
function.surjective (⇑e ∘ f) ↔ function.surjective f
source
@[simp]
theorem equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) :
function.bijective (f ∘ ⇑e) ↔ function.bijective f
source
@[simp]
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
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
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_empty (α : Sort u) [is_empty α] :
α ≃ empty

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

Equations
source
def equiv.equiv_empty_equiv (α : Sort u) :
α ≃ empty ≃ is_empty α

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

Equations
source
def equiv.false_equiv_empty  :
false ≃ empty

false is equivalent to empty.

Equations
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
source
def equiv.false_equiv_pempty  :
false ≃ pempty

false is equivalent to pempty.

Equations
source
def equiv.empty_equiv_pempty  :
empty ≃ pempty

empty is equivalent to pempty.

Equations
source
def equiv.pempty_equiv_pempty  :
pempty ≃ pempty

pempty types from any two universes are equivalent.

Equations
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
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
source
def equiv.true_equiv_punit  :
true ≃ punit

true is equivalent to punit.

Equations
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
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
source
@[simp]
theorem equiv.plift_symm_apply {α : Sort u} :
⇑(equiv.plift.symm) = plift.up
source
@[simp]
theorem equiv.pprod_equiv_prod_symm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :
⇑(equiv.pprod_equiv_prod.symm) x = ⟨x.fst, x.snd⟩
source
@[simp]
theorem equiv.pprod_equiv_prod_apply {α : Type u_1} {β : Type u_2} (x : pprod α β) :
⇑equiv.pprod_equiv_prod x = (x.fst, x.snd)
source
def equiv.pprod_equiv_prod {α : Type u_1} {β : Type u_2} :
pprod α β ≃ α × β

pprod α β is equivalent to α × β

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

equivalence of propositions is the same as iff

Equations
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
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
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
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.semiconj_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁) :
function.semiconj ⇑e f (⇑(e.conj) f)
source
theorem equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) :
function.semiconj₂ ⇑e f (⇑(e.arrow_congr e.conj) f)
source
@[protected, instance]
def equiv.arrow_congr.is_associative {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [is_associative α₁ f] :
is_associative β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)
source
@[protected, instance]
def equiv.arrow_congr.is_idempotent {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [is_idempotent α₁ f] :
is_idempotent β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)
source
@[protected, instance]
def equiv.arrow_congr.is_left_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [is_left_cancel α₁ f] :
is_left_cancel β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)
source
@[protected, instance]
def equiv.arrow_congr.is_right_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [is_right_cancel α₁ f] :
is_right_cancel β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)
source
def equiv.punit_equiv_punit  :
punit ≃ punit

punit sorts in any two universes are equivalent.

Equations
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
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
source
@[simp]
theorem equiv.fun_unique_symm_apply (α : Sort u_1) (β : Sort u_2) [unique α] :
⇑((equiv.fun_unique α β).symm) = function.const α
source
@[simp]
theorem equiv.fun_unique_apply (α : Sort u_1) (β : Sort u_2) [unique α] :
⇑(equiv.fun_unique α β) = function.eval (default α)
source
def equiv.punit_arrow_equiv (α : Sort u_1) :
(punit → α) ≃ α

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

Equations
source
def equiv.true_arrow_equiv (α : Sort u_1) :
(true → α) ≃ α

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

Equations
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
source
def equiv.empty_arrow_equiv_punit (α : Sort u_1) :
(empty → α) ≃ punit

The sort of maps from empty is equivalent to punit.

Equations
source
def equiv.pempty_arrow_equiv_punit (α : Sort u_1) :
(pempty → α) ≃ punit

The sort of maps from pempty is equivalent to punit.

Equations
source
def equiv.false_arrow_equiv_punit (α : Sort u_1) :
(false → α) ≃ punit

The sort of maps from false is equivalent to punit.

Equations
source
def equiv.prod_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
α₁ × β₁ ≃ α₂ × β₂

Product of two equivalences. If α₁ ≃ α₂ and β₁ ≃ β₂, then α₁ × β₁ ≃ α₂ × β₂.

Equations
source
@[simp]
theorem equiv.prod_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (x : α₁ × β₁) :
⇑(e₁.prod_congr e₂) x = prod.map ⇑e₁ ⇑e₂ x
source
@[simp]
theorem equiv.prod_congr_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
(e₁.prod_congr e₂).symm = e₁.symm.prod_congr e₂.symm
source
def equiv.prod_comm (α : Type u_1) (β : Type u_2) :
α × β ≃ β × α

Type product is commutative up to an equivalence: α × β ≃ β × α.

Equations
source
@[simp]
theorem equiv.prod_comm_apply (α : Type u_1) (β : Type u_2) (ᾰ : α × β) :
⇑(equiv.prod_comm α β) ᾰ = ᾰ.swap
source
@[simp]
theorem equiv.prod_comm_symm (α : Type u_1) (β : Type u_2) :
(equiv.prod_comm α β).symm = equiv.prod_comm β α
source
@[simp]
theorem equiv.prod_assoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) :
⇑((equiv.prod_assoc α β γ).symm) p = ((p.fst, p.snd.fst), p.snd.snd)
source
def equiv.prod_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α × β) × γ ≃ α × β × γ

Type product is associative up to an equivalence.

Equations
source
@[simp]
theorem equiv.prod_assoc_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : (α × β) × γ) :
⇑(equiv.prod_assoc α β γ) p = (p.fst.fst, p.fst.snd, p.snd)
source
@[simp]
theorem equiv.curry_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
⇑((equiv.curry α β γ).symm) = function.uncurry
source
def equiv.curry (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α × β → γ) ≃ (α → β → γ)

Functions on α × β are equivalent to functions α → β → γ.

Equations
source
@[simp]
theorem equiv.curry_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
⇑(equiv.curry α β γ) = function.curry
source
def equiv.prod_punit (α : Type u_1) :
α × punit ≃ α

punit is a right identity for type product up to an equivalence.

Equations
source
@[simp]
theorem equiv.prod_punit_apply (α : Type u_1) (p : α × punit) :
⇑(equiv.prod_punit α) p = p.fst
source
@[simp]
theorem equiv.prod_punit_symm_apply (α : Type u_1) (a : α) :
⇑((equiv.prod_punit α).symm) a = (a, punit.star)
source
def equiv.punit_prod (α : Type u_1) :
punit × α ≃ α

punit is a left identity for type product up to an equivalence.

Equations
source
@[simp]
theorem equiv.punit_prod_symm_apply (α : Type u_1) (ᾰ : α) :
⇑((equiv.punit_prod α).symm) ᾰ = (punit.star, ᾰ)
source
@[simp]
theorem equiv.punit_prod_apply (α : Type u_1) (ᾰ : punit × α) :
⇑(equiv.punit_prod α) ᾰ = ᾰ.snd
source
def equiv.prod_empty (α : Type u_1) :
α × empty ≃ empty

empty type is a right absorbing element for type product up to an equivalence.

Equations
source
def equiv.empty_prod (α : Type u_1) :
empty × α ≃ empty

empty type is a left absorbing element for type product up to an equivalence.

Equations
source
def equiv.prod_pempty (α : Type u_1) :
α × pempty ≃ pempty

pempty type is a right absorbing element for type product up to an equivalence.

Equations
source
def equiv.pempty_prod (α : Type u_1) :
pempty × α ≃ pempty

pempty type is a left absorbing element for type product up to an equivalence.

Equations
source
def equiv.psum_equiv_sum (α : Type u_1) (β : Type u_2) :
psum α β ≃ α ⊕ β

psum is equivalent to sum.

Equations
source
@[simp]
theorem equiv.sum_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ᾰ : α₁ ⊕ β₁) :
⇑(ea.sum_congr eb) ᾰ = sum.map ⇑ea ⇑eb ᾰ
source
def equiv.sum_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) :
α₁ ⊕ β₁ ≃ α₂ ⊕ β₂

If α ≃ α' and β ≃ β', then α ⊕ β ≃ α' ⊕ β'.

Equations
source
@[simp]
theorem equiv.sum_congr_trans {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) :
(e.sum_congr f).trans (g.sum_congr h) = (e.trans g).sum_congr (f.trans h)
source
@[simp]
theorem equiv.sum_congr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (f : γ ≃ δ) :
(e.sum_congr f).symm = e.symm.sum_congr f.symm
source
@[simp]
theorem equiv.sum_congr_refl {α : Type u_1} {β : Type u_2} :
(equiv.refl α).sum_congr (equiv.refl β) = equiv.refl (α ⊕ β)
source
def equiv.perm.sum_congr {α : Type u_1} {β : Type u_2} (ea : equiv.perm α) (eb : equiv.perm β) :
equiv.perm (α ⊕ β)

Combine a permutation of α and of β into a permutation of α ⊕ β.

Equations
source
@[simp]
theorem equiv.perm.sum_congr_apply {α : Type u_1} {β : Type u_2} (ea : equiv.perm α) (eb : equiv.perm β) (x : α ⊕ β) :
⇑(ea.sum_congr eb) x = sum.map ⇑ea ⇑eb x
source
@[simp]
theorem equiv.perm.sum_congr_trans {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) (g : equiv.perm α) (h : equiv.perm β) :
equiv.trans (e.sum_congr f) (g.sum_congr h) = equiv.perm.sum_congr (equiv.trans e g) (equiv.trans f h)
source
@[simp]
theorem equiv.perm.sum_congr_symm {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) :
equiv.symm (e.sum_congr f) = equiv.perm.sum_congr (equiv.symm e) (equiv.symm f)
source
@[simp]
theorem equiv.perm.sum_congr_refl {α : Type u_1} {β : Type u_2} :
equiv.perm.sum_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α ⊕ β)
source
def equiv.bool_equiv_punit_sum_punit  :
bool ≃ punit ⊕ punit

bool is equivalent the sum of two punits.

Equations
source
noncomputable def equiv.Prop_equiv_bool  :
Prop ≃ bool

Prop is noncomputably equivalent to bool.

Equations
source
@[simp]
theorem equiv.sum_comm_apply (α : Type u_1) (β : Type u_2) (ᾰ : α ⊕ β) :
⇑(equiv.sum_comm α β) ᾰ = ᾰ.swap
source
def equiv.sum_comm (α : Type u_1) (β : Type u_2) :
α ⊕ β ≃ β ⊕ α

Sum of types is commutative up to an equivalence.

Equations
source
@[simp]
theorem equiv.sum_comm_symm (α : Type u_1) (β : Type u_2) :
(equiv.sum_comm α β).symm = equiv.sum_comm β α
source
def equiv.sum_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ

Sum of types is associative up to an equivalence.

Equations
source
@[simp]
theorem equiv.sum_assoc_apply_in1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
⇑(equiv.sum_assoc α β γ) (sum.inl (sum.inl a)) = sum.inl a
source
@[simp]
theorem equiv.sum_assoc_apply_in2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
⇑(equiv.sum_assoc α β γ) (sum.inl (sum.inr b)) = sum.inr (sum.inl b)
source
@[simp]
theorem equiv.sum_assoc_apply_in3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
⇑(equiv.sum_assoc α β γ) (sum.inr c) = sum.inr (sum.inr c)
source
def equiv.sum_empty (α : Type u_1) (β : Type u_2) [is_empty β] :
α ⊕ β ≃ α

Sum with empty is equivalent to the original type.

Equations
source
@[simp]
theorem equiv.sum_empty_symm_apply (α : Type u_1) (β : Type u_2) [is_empty β] (val : α) :
⇑((equiv.sum_empty α β).symm) val = sum.inl val
source
@[simp]
theorem equiv.sum_empty_apply_inl {α : Type u_1} {β : Type u_2} [is_empty β] (a : α) :
⇑(equiv.sum_empty α β) (sum.inl a) = a
source
def equiv.empty_sum (α : Type u_1) (β : Type u_2) [is_empty α] :
α ⊕ β ≃ β

The sum of empty with any Sort* is equivalent to the right summand.

Equations
source
@[simp]
theorem equiv.empty_sum_symm_apply (α : Type u_1) (β : Type u_2) [is_empty α] (ᾰ : β) :
⇑((equiv.empty_sum α β).symm) ᾰ = sum.inr ᾰ
source
@[simp]
theorem equiv.empty_sum_apply_inr {α : Type u_1} {β : Type u_2} [is_empty α] (b : β) :
⇑(equiv.empty_sum α β) (sum.inr b) = b
source
def equiv.option_equiv_sum_punit (α : Type u_1) :
option α ≃ α ⊕ punit

option α is equivalent to α ⊕ punit

Equations
source
@[simp]
theorem equiv.option_equiv_sum_punit_none {α : Type u_1} :
⇑(equiv.option_equiv_sum_punit α) none = sum.inr punit.star
source
@[simp]
theorem equiv.option_equiv_sum_punit_some {α : Type u_1} (a : α) :
⇑(equiv.option_equiv_sum_punit α) (some a) = sum.inl a
source
@[simp]
theorem equiv.option_equiv_sum_punit_coe {α : Type u_1} (a : α) :
⇑(equiv.option_equiv_sum_punit α) ↑a = sum.inl a
source
@[simp]
theorem equiv.option_equiv_sum_punit_symm_inl {α : Type u_1} (a : α) :
⇑((equiv.option_equiv_sum_punit α).symm) (sum.inl a) = ↑a
source
@[simp]
theorem equiv.option_equiv_sum_punit_symm_inr {α : Type u_1} (a : punit) :
⇑((equiv.option_equiv_sum_punit α).symm) (sum.inr a) = none
source
@[simp]
theorem equiv.option_is_some_equiv_symm_apply_coe (α : Type u_1) (x : α) :
↑(⇑((equiv.option_is_some_equiv α).symm) x) = some x
source
@[simp]
theorem equiv.option_is_some_equiv_apply (α : Type u_1) (o : {x // ↥(x.is_some)}) :
⇑(equiv.option_is_some_equiv α) o = option.get _
source
def equiv.option_is_some_equiv (α : Type u_1) :
{x // ↥(x.is_some)} ≃ α

The set of x : option α such that is_some x is equivalent to α.

Equations
source
@[simp]
theorem equiv.pi_option_equiv_prod_apply {α : Type u_1} {β : option α → Type u_2} (f : Π (a : option α), β a) :
⇑equiv.pi_option_equiv_prod f = (f none, λ (a : α), f (some a))
source
@[simp]
theorem equiv.pi_option_equiv_prod_symm_apply {α : Type u_1} {β : option α → Type u_2} (x : β none × Π (a : α), β (some a)) (a : option α) :
⇑(equiv.pi_option_equiv_prod.symm) x a = a.cases_on x.fst x.snd
source
def equiv.pi_option_equiv_prod {α : Type u_1} {β : option α → Type u_2} :
(Π (a : option α), β a) ≃ β none × Π (a : α), β (some a)

The product over option α of β a is the binary product of the product over α of β (some α) and β none

Equations
source
def equiv.sum_equiv_sigma_bool (α β : Type u) :
α ⊕ β ≃ Σ (b : bool), cond b α β

α ⊕ β is equivalent to a sigma-type over bool. Note that this definition assumes α and β to be types from the same universe, so it cannot by used directly to transfer theorems about sigma types to theorems about sum types. In many cases one can use ulift to work around this difficulty.

Equations
source
@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
(⇑((equiv.sigma_preimage_equiv f).symm) x).fst = f x
source
def equiv.sigma_preimage_equiv {α : Type u_1} {β : Type u_2} (f : α → β) :
(Σ (y : β), {x // f x = y}) ≃ α

sigma_preimage_equiv f for f : α → β is the natural equivalence between the type of all fibres of f and the total space α.

Equations
source
@[simp]
theorem equiv.sigma_preimage_equiv_apply {α : Type u_1} {β : Type u_2} (f : α → β) (x : Σ (y : β), {x // f x = y}) :
⇑(equiv.sigma_preimage_equiv f) x = ↑(x.snd)
source
@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
↑((⇑((equiv.sigma_preimage_equiv f).symm) x).snd) = x
source
def equiv.sum_compl {α : Type u_1} (p : α → Prop) [decidable_pred p] :
{a // p a} ⊕ {a // ¬p a} ≃ α

For any predicate p on α, the sum of the two subtypes {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α.

See subtype_or_equiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily is_compl p q.

Equations
source
@[simp]
theorem equiv.sum_compl_apply_inl {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : {a // p a}) :
⇑(equiv.sum_compl p) (sum.inl x) = ↑x
source
@[simp]
theorem equiv.sum_compl_apply_inr {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : {a // ¬p a}) :
⇑(equiv.sum_compl p) (sum.inr x) = ↑x
source
@[simp]
theorem equiv.sum_compl_apply_symm_of_pos {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) (h : p a) :
⇑((equiv.sum_compl p).symm) a = sum.inl ⟨a, h⟩
source
@[simp]
theorem equiv.sum_compl_apply_symm_of_neg {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) (h : ¬p a) :
⇑((equiv.sum_compl p).symm) a = sum.inr ⟨a, h⟩
source
def equiv.subtype_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) (f : {x // ¬p x} ≃ {x // ¬q x}) :
equiv.perm α

Combines an equiv between two subtypes with an equiv between their complements to form a permutation.

Equations
source
def equiv.perm.subtype_congr {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :
equiv.perm ε

Combining permutations on ε that permute only inside or outside the subtype split induced by p : ε → Prop constructs a permutation on ε.

Equations
source
theorem equiv.perm.subtype_congr.apply {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : ε) :
⇑(ep.subtype_congr en) a = dite (p a) (λ (h : p a), ↑(⇑ep ⟨a, h⟩)) (λ (h : ¬p a), ↑(⇑en ⟨a, h⟩))
source
@[simp]
theorem equiv.perm.subtype_congr.left_apply {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : p a) :
⇑(ep.subtype_congr en) a = ↑(⇑ep ⟨a, h⟩)
source
@[simp]
theorem equiv.perm.subtype_congr.left_apply_subtype {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : {a // p a}) :
⇑(ep.subtype_congr en) ↑a = ↑(⇑ep a)
source
@[simp]
theorem equiv.perm.subtype_congr.right_apply {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : ¬p a) :
⇑(ep.subtype_congr en) a = ↑(⇑en ⟨a, h⟩)
source
@[simp]
theorem equiv.perm.subtype_congr.right_apply_subtype {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : {a // ¬p a}) :
⇑(ep.subtype_congr en) ↑a = ↑(⇑en a)
source
@[simp]
theorem equiv.perm.subtype_congr.refl {ε : Type u_1} {p : ε → Prop} [decidable_pred p] :
equiv.perm.subtype_congr (equiv.refl {a // p a}) (equiv.refl {a // ¬p a}) = equiv.refl ε
source
@[simp]
theorem equiv.perm.subtype_congr.symm {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :
equiv.symm (ep.subtype_congr en) = equiv.perm.subtype_congr (equiv.symm ep) (equiv.symm en)
source
@[simp]
theorem equiv.perm.subtype_congr.trans {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep ep' : equiv.perm {a // p a}) (en en' : equiv.perm {a // ¬p a}) :
equiv.trans (ep.subtype_congr en) (ep'.subtype_congr en') = equiv.perm.subtype_congr (equiv.trans ep ep') (equiv.trans en en')
source
@[simp]
theorem equiv.subtype_preimage_symm_apply_coe {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) :
↑(⇑((equiv.subtype_preimage p x₀).symm) x) a = dite (p a) (λ (h : p a), x₀ ⟨a, h⟩) (λ (h : ¬p a), x ⟨a, h⟩)
source
@[simp]
theorem equiv.subtype_preimage_apply {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) (x : {x // x ∘ coe = x₀}) (a : {a // ¬p a}) :
⇑(equiv.subtype_preimage p x₀) x a = ↑x ↑a
source
def equiv.subtype_preimage {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) :
{x // x ∘ coe = x₀} ≃ ({a // ¬p a} → β)

For a fixed function x₀ : {a // p a} → β defined on a subtype of α, the subtype of functions x : α → β that agree with x₀ on the subtype {a // p a} is naturally equivalent to the type of functions {a // ¬ p a} → β.

Equations
source
theorem equiv.subtype_preimage_symm_apply_coe_pos {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) (h : p a) :
↑(⇑((equiv.subtype_preimage p x₀).symm) x) a = x₀ ⟨a, h⟩
source
theorem equiv.subtype_preimage_symm_apply_coe_neg {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) (h : ¬p a) :
↑(⇑((equiv.subtype_preimage p x₀).symm) x) a = x ⟨a, h⟩
source
def equiv.Pi_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
source
def equiv.Pi_curry {α : Type u_1} {β : α → Type u_2} (γ : Π (a : α), β a → Type u_3) :
(Π (x : Σ (i : α), β i), γ x.fst x.snd) ≃ Π (a : α) (b : β a), γ a b

Dependent curry equivalence: the type of dependent functions on Σ i, β i is equivalent to the type of dependent functions of two arguments (i.e., functions to the space of functions).

This is sigma.curry and sigma.uncurry together as an equiv.

Equations
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
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
@[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
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
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
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
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
source
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
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
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
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
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
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
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
source
def equiv.prod_congr_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) :
β₁ × α₁ ≃ β₂ × α₁

A family of equivalences Π (a : α₁), β₁ ≃ β₂ generates an equivalence between β₁ × α₁ and β₂ × α₁.

Equations
source
@[simp]
theorem equiv.prod_congr_left_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) (b : β₁) (a : α₁) :
⇑(equiv.prod_congr_left e) (b, a) = (⇑(e a) b, a)
source
theorem equiv.prod_congr_refl_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ ≃ β₂) :
e.prod_congr (equiv.refl α₁) = equiv.prod_congr_left (λ (_x : α₁), e)
source
def equiv.prod_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) :
α₁ × β₁ ≃ α₁ × β₂

A family of equivalences Π (a : α₁), β₁ ≃ β₂ generates an equivalence between α₁ × β₁ and α₁ × β₂.

Equations
source
@[simp]
theorem equiv.prod_congr_right_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) (a : α₁) (b : β₁) :
⇑(equiv.prod_congr_right e) (a, b) = (a, ⇑(e a) b)
source
theorem equiv.prod_congr_refl_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ ≃ β₂) :
(equiv.refl α₁).prod_congr e = equiv.prod_congr_right (λ (_x : α₁), e)
source
@[simp]
theorem equiv.prod_congr_left_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) :
(equiv.prod_congr_left e).trans (equiv.prod_comm β₂ α₁) = (equiv.prod_comm β₁ α₁).trans (equiv.prod_congr_right e)
source
@[simp]
theorem equiv.prod_congr_right_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) :
(equiv.prod_congr_right e).trans (equiv.prod_comm α₁ β₂) = (equiv.prod_comm α₁ β₁).trans (equiv.prod_congr_left e)
source
theorem equiv.sigma_congr_right_sigma_equiv_prod {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) :
(equiv.sigma_congr_right e).trans (equiv.sigma_equiv_prod α₁ β₂) = (equiv.sigma_equiv_prod α₁ β₁).trans (equiv.prod_congr_right e)
source
theorem equiv.sigma_equiv_prod_sigma_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) :
(equiv.sigma_equiv_prod α₁ β₁).symm.trans (equiv.sigma_congr_right e) = (equiv.prod_congr_right e).trans (equiv.sigma_equiv_prod α₁ β₂).symm
source
@[simp]
theorem equiv.prod_shear_symm_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) :
⇑((e₁.prod_shear e₂).symm) = λ (y : α₂ × β₂), (⇑(e₁.symm) y.fst, ⇑((e₂ (⇑(e₁.symm) y.fst)).symm) y.snd)
source
@[simp]
theorem equiv.prod_shear_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) :
⇑(e₁.prod_shear e₂) = λ (x : α₁ × β₁), (⇑e₁ x.fst, ⇑(e₂ x.fst) x.snd)
source
def equiv.prod_shear {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : α₁ → β₁ ≃ β₂) :
α₁ × β₁ ≃ α₂ × β₂

A variation on equiv.prod_congr where the equivalence in the second component can depend on the first component. A typical example is a shear mapping, explaining the name of this declaration.

Equations
source
def equiv.perm.prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) :
equiv.perm (α₁ × β₁)

prod_extend_right a e extends e : perm β to perm (α × β) by sending (a, b) to (a, e b) and keeping the other (a', b) fixed.

Equations
source
@[simp]
theorem equiv.perm.prod_extend_right_apply_eq {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (b : β₁) :
⇑(equiv.perm.prod_extend_right a e) (a, b) = (a, ⇑e b)
source
theorem equiv.perm.prod_extend_right_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (e : equiv.perm β₁) {a a' : α₁} (h : a' ≠ a) (b : β₁) :
⇑(equiv.perm.prod_extend_right a e) (a', b) = (a', b)
source
theorem equiv.perm.eq_of_prod_extend_right_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] {e : equiv.perm β₁} {a a' : α₁} {b : β₁} (h : ⇑(equiv.perm.prod_extend_right a e) (a', b) ≠ (a', b)) :
a' = a
source
@[simp]
theorem equiv.perm.fst_prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (ab : α₁ × β₁) :
(⇑(equiv.perm.prod_extend_right a e) ab).fst = ab.fst
source
def equiv.arrow_prod_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(γ → α × β) ≃ (γ → α) × (γ → β)

The type of functions to a product α × β is equivalent to the type of pairs of functions γ → α and γ → β.

Equations
source
def equiv.sum_arrow_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α ⊕ β → γ) ≃ (α → γ) × (β → γ)

The type of functions on a sum type α ⊕ β is equivalent to the type of pairs of functions on α and on β.

Equations
source
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ) (a : α) :
(⇑(equiv.sum_arrow_equiv_prod_arrow α β γ) f).fst a = f (sum.inl a)
source
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ) (b : β) :
(⇑(equiv.sum_arrow_equiv_prod_arrow α β γ) f).snd b = f (sum.inr b)
source
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) (a : α) :
⇑((equiv.sum_arrow_equiv_prod_arrow α β γ).symm) (f, g) (sum.inl a) = f a
source
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) (b : β) :
⇑((equiv.sum_arrow_equiv_prod_arrow α β γ).symm) (f, g) (sum.inr b) = g b
source
def equiv.sum_prod_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α ⊕ β) × γ ≃ α × γ ⊕ β × γ

Type product is right distributive with respect to type sum up to an equivalence.

Equations
source
@[simp]
theorem equiv.sum_prod_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
⇑(equiv.sum_prod_distrib α β γ) (sum.inl a, c) = sum.inl (a, c)
source
@[simp]
theorem equiv.sum_prod_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) (c : γ) :
⇑(equiv.sum_prod_distrib α β γ) (sum.inr b, c) = sum.inr (b, c)
source
def equiv.prod_sum_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
α × (β ⊕ γ) ≃ α × β ⊕ α × γ

Type product is left distributive with respect to type sum up to an equivalence.

Equations
source
@[simp]
theorem equiv.prod_sum_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (b : β) :
⇑(equiv.prod_sum_distrib α β γ) (a, sum.inl b) = sum.inl (a, b)
source
@[simp]
theorem equiv.prod_sum_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
⇑(equiv.prod_sum_distrib α β γ) (a, sum.inr c) = sum.inr (a, c)
source
def equiv.sigma_prod_distrib {ι : Type u_1} (α : ι → Type u_2) (β : Type u_3) :
(Σ (i : ι), α i) × β ≃ Σ (i : ι), α i × β

The product of an indexed sum of types (formally, a sigma-type Σ i, α i) by a type β is equivalent to the sum of products Σ i, (α i × β).

Equations
source
def equiv.bool_prod_equiv_sum (α : Type u) :
bool × α ≃ α ⊕ α

The product bool × α is equivalent to α ⊕ α.

Equations
source
def equiv.bool_arrow_equiv_prod (α : Type u) :
(bool → α) ≃ α × α

The function type bool → α is equivalent to α × α.

Equations
source
@[simp]
theorem equiv.bool_arrow_equiv_prod_apply (α : Type u) (f : bool → α) :
⇑(equiv.bool_arrow_equiv_prod α) f = (f tt, f ff)
source
@[simp]
theorem equiv.bool_arrow_equiv_prod_symm_apply (α : Type u) (p : α × α) (b : bool) :
⇑((equiv.bool_arrow_equiv_prod α).symm) p b = cond b p.fst p.snd
source
def equiv.nat_equiv_nat_sum_punit  :
ℕ ≃ ℕ ⊕ punit

The set of natural numbers is equivalent to ℕ ⊕ punit.

Equations
source
def equiv.nat_sum_punit_equiv_nat  :
ℕ ⊕ punit ≃ ℕ

ℕ ⊕ punit is equivalent to ℕ.

Equations
source
def equiv.int_equiv_nat_sum_nat  :
ℤ ≃ ℕ ⊕ ℕ

The type of integer numbers is equivalent to ℕ ⊕ ℕ.

Equations
source
def equiv.list_equiv_of_equiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
list α ≃ list β

An equivalence between α and β generates an equivalence between list α and list β.

Equations
source
def equiv.fin_equiv_subtype (n : ℕ) :
fin n ≃ {m // m < n}

fin n is equivalent to {m // m < n}.

Equations
source
def equiv.unique_congr {α : Sort u} {β : Sort v} (e : α ≃ β) :
unique α ≃ unique β

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

Equations
source
theorem equiv.is_empty_congr {α : Sort u} {β : Sort v} (e : α ≃ β) :
is_empty α ↔ is_empty β

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

source
@[protected]
theorem equiv.is_empty {α : Sort u} {β : Sort v} (e : α ≃ β) [is_empty β] :
is_empty α
source
def equiv.subtype_equiv {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (⇑e a)) :
{a // p a} ≃ {b // q b}

If α is equivalent to β and the predicates p : α → Prop and q : β → Prop are equivalent at corresponding points, then {a // p a} is equivalent to {b // q b}. For the statement where α = β, that is, e : perm α, see perm.subtype_perm.

Equations
source
@[simp]
theorem equiv.subtype_equiv_refl {α : Sort u} {p : α → Prop} (h : (∀ (a : α), p a ↔ p (⇑(equiv.refl α) a)) := _) :
(equiv.refl α).subtype_equiv h = equiv.refl {a // p a}
source
@[simp]
theorem equiv.subtype_equiv_symm {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (⇑e a)) :
(e.subtype_equiv h).symm = e.symm.subtype_equiv _
source
@[simp]
theorem equiv.subtype_equiv_trans {α : Sort u} {β : Sort v} {γ : Sort w} {p : α → Prop} {q : β → Prop} {r : γ → Prop} (e : α ≃ β) (f : β ≃ γ) (h : ∀ (a : α), p a ↔ q (⇑e a)) (h' : ∀ (b : β), q b ↔ r (⇑f b)) :
(e.subtype_equiv h).trans (f.subtype_equiv h') = (e.trans f).subtype_equiv _
source
@[simp]
theorem equiv.subtype_equiv_apply {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (⇑e a)) (x : {x // p x}) :
⇑(e.subtype_equiv h) x = ⟨⇑e ↑x, _⟩
source
@[simp]
theorem equiv.subtype_equiv_right_symm_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (y : {b // (λ (x : α), q x) b}) :
↑(⇑((equiv.subtype_equiv_right e).symm) y) = ↑y
source
def equiv.subtype_equiv_right {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) :
{x // p x} ≃ {x // q x}

If two predicates p and q are pointwise equivalent, then {x // p x} is equivalent to {x // q x}.

Equations
source
@[simp]
theorem equiv.subtype_equiv_right_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (x : {a // (λ (x : α), p x) a}) :
↑(⇑(equiv.subtype_equiv_right e) x) = ↑x
source
def equiv.subtype_equiv_of_subtype {α : Sort u} {β : Sort v} {p : β → Prop} (e : α ≃ β) :
{a // p (⇑e a)} ≃ {b // p b}

If α ≃ β, then for any predicate p : β → Prop the subtype {a // p (e a)} is equivalent to the subtype {b // p b}.

Equations
source
def equiv.subtype_equiv_of_subtype' {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) :
{a // p a} ≃ {b // p (⇑(e.symm) b)}

If α ≃ β, then for any predicate p : α → Prop the subtype {a // p a} is equivalent to the subtype {b // p (e.symm b)}. This version is used by equiv_rw.

Equations
source
def equiv.subtype_equiv_prop {α : Type u_1} {p q : α → Prop} (h : p = q) :
subtype p ≃ subtype q

If two predicates are equal, then the corresponding subtypes are equivalent.

Equations
source
def equiv.subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : subtype p → Prop) :
subtype q ≃ {a // ∃ (h : p a), q ⟨a, h⟩}

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This version allows the “inner” predicate to depend on h : p a.

Equations
source
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_exists_apply {α : Type u} (p : α → Prop) (q : subtype p → Prop) (a : subtype q) :
↑(⇑(equiv.subtype_subtype_equiv_subtype_exists p q) a) = ↑a
source
def equiv.subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
{x // q x.val} ≃ {x // p x ∧ q x}

A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates.

Equations
source
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_inter_apply {α : Type u} (p q : α → Prop) (a : {x // q x.val}) :
↑(⇑(equiv.subtype_subtype_equiv_subtype_inter p q) a) = ↑a
source
def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) :
{x // q x.val} ≃ subtype q

If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.

Equations
source
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_apply {α : Type u} {p q : α → Prop} (h : ∀ (x : α), q x → p x) (a : {x // q x.val}) :
↑(⇑(equiv.subtype_subtype_equiv_subtype h) a) = ↑a
source
def equiv.subtype_univ_equiv {α : Type u} {p : α → Prop} (h : ∀ (x : α), p x) :
subtype p ≃ α

If a proposition holds for all elements, then the subtype is equivalent to the original type.

Equations
source
@[simp]
theorem equiv.subtype_univ_equiv_symm_apply {α : Type u} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) :
⇑((equiv.subtype_univ_equiv h).symm) x = ⟨x, _⟩
source
@[simp]
theorem equiv.subtype_univ_equiv_apply {α : Type u} {p : α → Prop} (h : ∀ (x : α), p x) (x : subtype p) :
⇑(equiv.subtype_univ_equiv h) x = ↑x
source
def equiv.subtype_sigma_equiv {α : Type u} (p : α → Type v) (q : α → Prop) :
{y // q y.fst} ≃ Σ (x : subtype q), p x.val

A subtype of a sigma-type is a sigma-type over a subtype.

Equations
source
def equiv.sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop) (h : ∀ (x : α), p x → q x) :
(Σ (x : subtype q), p ↑x) ≃ Σ (x : α), p x

A sigma type over a subtype is equivalent to the sigma set over the original type, if the fiber is empty outside of the subset

Equations
source
def equiv.sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop) (h : ∀ (x : α), p (f x)) :
(Σ (y : subtype p), {x // f x = ↑y}) ≃ α

If a predicate p : β → Prop is true on the range of a map f : α → β, then Σ y : {y // p y}, {x // f x = y} is equivalent to α.

Equations
source
def equiv.sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β) {p : α → Prop} {q : β → Prop} (h : ∀ (x : α), p x ↔ q (f x)) :
(Σ (y : subtype q), {x // f x = ↑y}) ≃ subtype p

If for each x we have p x ↔ q (f x), then Σ y : {y // q y}, f ⁻¹' {y} is equivalent to {x // p x}.

Equations
source
def equiv.sigma_option_equiv_of_some {α : Type u} (p : option α → Type v) (h : p none → false) :
(Σ (x : option α), p x) ≃ Σ (x : α), p (some x)

A sigma type over an option is equivalent to the sigma set over the original type, if the fiber is empty at none.

Equations
source
def equiv.pi_equiv_subtype_sigma (ι : Type u_1) (π : ι → Type u_2) :
(Π (i : ι), π i) ≃ {f // ∀ (i : ι), (f i).fst = i}

The pi-type Π i, π i is equivalent to the type of sections f : ι → Σ i, π i of the sigma type such that for all i we have (f i).fst = i.

Equations
source
def equiv.subtype_pi_equiv_pi {α : Sort u} {β : α → Sort v} {p : Π (a : α), β a → Prop} :
{f // ∀ (a : α), p a (f a)} ≃ Π (a : α), {b // p a b}

The set of functions f : Π a, β a such that for all a we have p a (f a) is equivalent to the set of functions Π a, {b : β a // p a b}.

Equations
source
def equiv.subtype_prod_equiv_prod {α : Type u} {β : Type v} {p : α → Prop} {q : β → Prop} :
{c // p c.fst ∧ q c.snd} ≃ {a // p a} × {b // q b}

A subtype of a product defined by componentwise conditions is equivalent to a product of subtypes.

Equations
source
def equiv.subtype_prod_equiv_sigma_subtype {α : Type u_1} {β : Type u_2} (p : α → β → Prop) :
{x // p x.fst x.snd} ≃ Σ (a : α), {b // p a b}

A subtype of a prod is equivalent to a sigma type whose fibers are subtypes.

Equations
source
def equiv.pi_equiv_pi_subtype_prod {α : Type u_1} (p : α → Prop) (β : α → Type u_2) [decidable_pred p] :
(Π (i : α), β i) ≃ (Π (i : {x // p x}), β ↑i) × Π (i : {x // ¬p x}), β ↑i

The type Π (i : α), β i can be split as a product by separating the indices in α depending on whether they satisfy a predicate p or not.

Equations
source
@[simp]
theorem equiv.pi_equiv_pi_subtype_prod_symm_apply {α : Type u_1} (p : α → Prop) (β : α → Type u_2) [decidable_pred p] (f : (Π (i : {x // p x}), β ↑i) × Π (i : {x // ¬p x}), β ↑i) (x : α) :
⇑((equiv.pi_equiv_pi_subtype_prod p β).symm) f x = dite (p x) (λ (h : p x), f.fst ⟨x, h⟩) (λ (h : ¬p x), f.snd ⟨x, h⟩)
source
@[simp]
theorem equiv.pi_equiv_pi_subtype_prod_apply {α : Type u_1} (p : α → Prop) (β : α → Type u_2) [decidable_pred p] (f : Π (i : α), β i) :
⇑(equiv.pi_equiv_pi_subtype_prod p β) f = (λ (x : {x // p x}), f ↑x, λ (x : {x // ¬p x}), f ↑x)
source
def equiv.subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) :
{g // g ∘ coe = f} ≃ Y

The type of all functions X → Y with prescribed values for all x' ≠ x is equivalent to the codomain Y.

Equations
source
@[simp]
theorem equiv.coe_subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) :
⇑(equiv.subtype_equiv_codomain f) = λ (g : {g // g ∘ coe = f}), ↑g x
source
@[simp]
theorem equiv.subtype_equiv_codomain_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) (g : {g // g ∘ coe = f}) :
⇑(equiv.subtype_equiv_codomain f) g = ↑g x
source
theorem equiv.coe_subtype_equiv_codomain_symm {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) :
⇑((equiv.subtype_equiv_codomain f).symm) = λ (y : Y), ⟨λ (x' : X), dite (x' ≠ x) (λ (h : x' ≠ x), f ⟨x', h⟩) (λ (h : ¬x' ≠ x), y), _⟩
source
@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) (y : Y) (x' : X) :
↑(⇑((equiv.subtype_equiv_codomain f).symm) y) x' = dite (x' ≠ x) (λ (h : x' ≠ x), f ⟨x', h⟩) (λ (h : ¬x' ≠ x), y)
source
@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply_eq {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) (y : Y) :
↑(⇑((equiv.subtype_equiv_codomain f).symm) y) x = y
source
theorem equiv.subtype_equiv_codomain_symm_apply_ne {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' ≠ x} → Y) (y : Y) (x' : X) (h : x' ≠ x) :
↑(⇑((equiv.subtype_equiv_codomain f).symm) y) x' = f ⟨x', h⟩
source
noncomputable def equiv.of_bijective {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : function.bijective f) :
α ≃ β

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

Equations
source
@[simp]
theorem equiv.of_bijective_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : function.bijective f) (ᾰ : α) :
⇑(equiv.of_bijective f hf) ᾰ = f ᾰ
source
theorem equiv.of_bijective_apply_symm_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : function.bijective f) (x : β) :
f (⇑((equiv.of_bijective f hf).symm) x) = x
source
@[simp]
theorem equiv.of_bijective_symm_apply_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : function.bijective f) (x : α) :
⇑((equiv.of_bijective f hf).symm) (f x) = x
source
def equiv.perm.extend_domain {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) :
equiv.perm β'

Extend the domain of e : equiv.perm α to one that is over β via f : α → subtype p, where p : β → Prop, permuting only the b : β that satisfy p b. This can be used to extend the domain across a function f : α → β, keeping everything outside of set.range f fixed. For this use-case equiv given by f can be constructed by equiv.of_left_inverse' or equiv.of_left_inverse when there is a known inverse, or equiv.of_injective in the general case.`.

Equations
source
@[simp]
theorem equiv.perm.extend_domain_apply_image {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) (a : α') :
⇑(e.extend_domain f) ↑(⇑f a) = ↑(⇑f (⇑e a))
source
theorem equiv.perm.extend_domain_apply_subtype {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) {b : β'} (h : p b) :
⇑(e.extend_domain f) b = ↑(⇑f (⇑e (⇑(f.symm) ⟨b, h⟩)))
source
theorem equiv.perm.extend_domain_apply_not_subtype {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) {b : β'} (h : ¬p b) :
⇑(e.extend_domain f) b = b
source
@[simp]
theorem equiv.perm.extend_domain_refl {α' : Type u_1} {β' : Type u_2} {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) :
equiv.perm.extend_domain (equiv.refl α') f = equiv.refl β'
source
@[simp]
theorem equiv.perm.extend_domain_symm {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) :
equiv.symm (e.extend_domain f) = equiv.perm.extend_domain (equiv.symm e) f
source
theorem equiv.perm.extend_domain_trans {α' : Type u_1} {β' : Type u_2} {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) (e e' : equiv.perm α') :
equiv.trans (e.extend_domain f) (e'.extend_domain f) = equiv.perm.extend_domain (equiv.trans e e') f
source
def equiv.subtype_quotient_equiv_quotient_subtype {α : Sort u} (p₁ : α → Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : subtype p₁), setoid.r x y ↔ ↑x ≈ ↑y) :
{x // p₂ x} ≃ quotient s₂

Subtype of the quotient is equivalent to the quotient of the subtype. Let α be a setoid with equivalence relation ~. Let p₂ be a predicate on the quotient type α/~, and p₁ be the lift of this predicate to α: p₁ a ↔ p₂ ⟦a⟧. Let ~₂ be the restriction of ~ to {x // p₁ x}. Then {x // p₂ x} is equivalent to the quotient of {x // p₁ x} by ~₂.

Equations
source
def equiv.swap_core {α : Sort u} [decidable_eq α] (a b r : α) :
α

A helper function for equiv.swap.

Equations
source
theorem equiv.swap_core_self {α : Sort u} [decidable_eq α] (r a : α) :
equiv.swap_core a a r = r
source
theorem equiv.swap_core_swap_core {α : Sort u} [decidable_eq α] (r a b : α) :
equiv.swap_core a b (equiv.swap_core a b r) = r
source
theorem equiv.swap_core_comm {α : Sort u} [decidable_eq α] (r a b : α) :
equiv.swap_core a b r = equiv.swap_core b a r
source
def equiv.swap {α : Sort u} [decidable_eq α] (a b : α) :
equiv.perm α

swap a b is the permutation that swaps a and b and leaves other values as is.

Equations
source
@[simp]
theorem equiv.swap_self {α : Sort u} [decidable_eq α] (a : α) :
equiv.swap a a = equiv.refl α
source
theorem equiv.swap_comm {α : Sort u} [decidable_eq α] (a b : α) :
equiv.swap a b = equiv.swap b a
source
theorem equiv.swap_apply_def {α : Sort u} [decidable_eq α] (a b x : α) :
⇑(equiv.swap a b) x = ite (x = a) b (ite (x = b) a x)
source
@[simp]
theorem equiv.swap_apply_left {α : Sort u} [decidable_eq α] (a b : α) :
⇑(equiv.swap a b) a = b
source
@[simp]
theorem equiv.swap_apply_right {α : Sort u} [decidable_eq α] (a b : α) :
⇑(equiv.swap a b) b = a
source
theorem equiv.swap_apply_of_ne_of_ne {α : Sort u} [decidable_eq α] {a b x : α} :
x ≠ a → x ≠ b → ⇑(equiv.swap a b) x = x
source
@[simp]
theorem equiv.swap_swap {α : Sort u} [decidable_eq α] (a b : α) :
equiv.trans (equiv.swap a b) (equiv.swap a b) = equiv.refl α
source
@[simp]
theorem equiv.symm_swap {α : Sort u} [decidable_eq α] (a b : α) :
equiv.symm (equiv.swap a b) = equiv.swap a b
source
@[simp]
theorem equiv.swap_eq_refl_iff {α : Sort u} [decidable_eq α] {x y : α} :
equiv.swap x y = equiv.refl α ↔ x = y
source
theorem equiv.swap_comp_apply {α : Sort u} [decidable_eq α] {a b x : α} (π : equiv.perm α) :
⇑(equiv.trans π (equiv.swap a b)) x = ite (⇑π x = a) b (ite (⇑π x = b) a (⇑π x))
source
theorem equiv.swap_eq_update {α : Sort u} [decidable_eq α] (i j : α) :
⇑(equiv.swap i j) = function.update (function.update id j i) i j
source
theorem equiv.comp_swap_eq_update {α : Sort u} {β : Sort v} [decidable_eq α] (i j : α) (f : α → β) :
f ∘ ⇑(equiv.swap i j) = function.update (function.update f j (f i)) i (f j)
source
@[simp]
theorem equiv.symm_trans_swap_trans {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : α) (e : α ≃ β) :
(e.symm.trans (equiv.swap a b)).trans e = equiv.swap (⇑e a) (⇑e b)
source
@[simp]
theorem equiv.trans_swap_trans_symm {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : β) (e : α ≃ β) :
(e.trans (equiv.swap a b)).trans e.symm = equiv.swap (⇑(e.symm) a) (⇑(e.symm) b)
source
@[simp]
theorem equiv.swap_apply_self {α : Sort u} [decidable_eq α] (i j a : α) :
⇑(equiv.swap i j) (⇑(equiv.swap i j) a) = a
source
theorem equiv.apply_swap_eq_self {α : Sort u} {β : Sort v} [decidable_eq α] {v : α → β} {i j : α} (hv : v i = v j) (k : α) :
v (⇑(equiv.swap i j) k) = v k

A function is invariant to a swap if it is equal at both elements

source
theorem equiv.swap_apply_eq_iff {α : Sort u} [decidable_eq α] {x y z w : α} :
⇑(equiv.swap x y) z = w ↔ z = ⇑(equiv.swap x y) w
source
theorem equiv.swap_apply_ne_self_iff {α : Sort u} [decidable_eq α] {a b x : α} :
⇑(equiv.swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
source
@[simp]
theorem equiv.perm.sum_congr_swap_refl {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : α) :
(equiv.swap i j).sum_congr (equiv.refl β) = equiv.swap (sum.inl i) (sum.inl j)
source
@[simp]
theorem equiv.perm.sum_congr_refl_swap {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : β) :
equiv.perm.sum_congr (equiv.refl α) (equiv.swap i j) = equiv.swap (sum.inr i) (sum.inr j)
source
def equiv.set_value {α : Sort u} {β : Sort v} [decidable_eq α] (f : α ≃ β) (a : α) (b : β) :
α ≃ β

Augment an equivalence with a prescribed mapping f a = b

Equations
source
@[simp]
theorem equiv.set_value_eq {α : Sort u} {β : Sort v} [decidable_eq α] (f : α ≃ β) (a : α) (b : β) :
⇑(f.set_value a b) a = b
source
theorem plift.eq_up_iff_down_eq {α : Sort u} {x : plift α} {y : α} :
x = {down := y} ↔ x.down = y
source
theorem function.injective.map_swap {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α → β} (hf : function.injective f) (x y z : α) :
f (⇑(equiv.swap x y) z) = ⇑(equiv.swap (f x) (f y)) (f z)
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
@[simp]
theorem equiv.Pi_congr_left'_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) (f : Π (a : α), P a) (x : β) :
⇑(equiv.Pi_congr_left' P e) f x = f (⇑(e.symm) x)
source
def equiv.Pi_congr_left' {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) :
(Π (a : α), P a) ≃ Π (b : β), P (⇑(e.symm) b)

Transport dependent functions through an equivalence of the base space.

Equations
source
@[simp]
theorem equiv.Pi_congr_left'_symm_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) (f : Π (b : β), P (⇑(e.symm) b)) (x : α) :
⇑((equiv.Pi_congr_left' P e).symm) f x = _.mpr (f (⇑e x))
source
def equiv.Pi_congr_left {α : Sort u} {β : Sort v} (P : β → Sort w) (e : α ≃ β) :
(Π (a : α), P (⇑e a)) ≃ Π (b : β), P b

Transporting dependent functions through an equivalence of the base, expressed as a "simplification".

Equations
source
def equiv.Pi_congr {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (a : α), W a ≃ Z (⇑h₁ a)) :
(Π (a : α), W a) ≃ Π (b : β), Z b

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibers.

Equations
source
@[simp]
theorem equiv.coe_Pi_congr_symm {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (a : α), W a ≃ Z (⇑h₁ a)) :
⇑((h₁.Pi_congr h₂).symm) = λ (f : Π (b : β), Z b) (a : α), ⇑((h₂ a).symm) (f (⇑h₁ a))
source
theorem equiv.Pi_congr_symm_apply {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (a : α), W a ≃ Z (⇑h₁ a)) (f : Π (b : β), Z b) :
⇑((h₁.Pi_congr h₂).symm) f = λ (a : α), ⇑((h₂ a).symm) (f (⇑h₁ a))
source
@[simp]
theorem equiv.Pi_congr_apply_apply {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (a : α), W a ≃ Z (⇑h₁ a)) (f : Π (a : α), W a) (a : α) :
⇑(h₁.Pi_congr h₂) f (⇑h₁ a) = ⇑(h₂ a) (f a)
source
def equiv.Pi_congr' {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (b : β), W (⇑(h₁.symm) b) ≃ Z b) :
(Π (a : α), W a) ≃ Π (b : β), Z b

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibres.

Equations
source
@[simp]
theorem equiv.coe_Pi_congr' {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (b : β), W (⇑(h₁.symm) b) ≃ Z b) :
⇑(h₁.Pi_congr' h₂) = λ (f : Π (a : α), W a) (b : β), ⇑(h₂ b) (f (⇑(h₁.symm) b))
source
theorem equiv.Pi_congr'_apply {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (b : β), W (⇑(h₁.symm) b) ≃ Z b) (f : Π (a : α), W a) :
⇑(h₁.Pi_congr' h₂) f = λ (b : β), ⇑(h₂ b) (f (⇑(h₁.symm) b))
source
@[simp]
theorem equiv.Pi_congr'_symm_apply_symm_apply {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : Π (b : β), W (⇑(h₁.symm) b) ≃ Z b) (f : Π (b : β), Z b) (b : β) :
⇑((h₁.Pi_congr' h₂).symm) f (⇑(h₁.symm) b) = ⇑((h₂ b).symm) (f b)
source
theorem function.injective.swap_apply {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] {f : α → β} (hf : function.injective f) (x y z : α) :
⇑(equiv.swap (f x) (f y)) (f z) = f (⇑(equiv.swap x y) z)
source
theorem function.injective.swap_comp {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] {f : α → β} (hf : function.injective f) (x y : α) :
⇑(equiv.swap (f x) (f y)) ∘ f = f ∘ ⇑(equiv.swap x y)
source
def equiv_of_unique_of_unique {α : Sort u} {β : Sort v} [unique α] [unique β] :
α ≃ β

If both α and β are singletons, then α ≃ β.

Equations
source
def equiv_punit_of_unique {α : Sort u} [unique α] :
α ≃ punit

If α is a singleton, then it is equivalent to any punit.

Equations
source
def subsingleton_prod_self_equiv {α : Type u_1} [subsingleton α] :
α × α ≃ α

If α is a subsingleton, then it is equivalent to α × α.

Equations
source
def equiv_of_subsingleton_of_subsingleton {α : Sort u} {β : Sort v} [subsingleton α] [subsingleton β] (f : α → β) (g : β → α) :
α ≃ β

To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.

Equations
source
noncomputable def equiv.punit_of_nonempty_of_subsingleton {α : Sort u_1} [h : nonempty α] [subsingleton α] :
α ≃ punit

A nonempty subsingleton type is (noncomputably) equivalent to punit.

Equations
source
def unique_unique_equiv {α : Sort u} :
unique (unique α) ≃ unique α

unique (unique α) is equivalent to unique α.

Equations
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
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
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
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
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
source
theorem function.update_comp_equiv {α : Sort u_1} {β : Sort u_2} {α' : Sort u_3} [decidable_eq α'] [decidable_eq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) :
function.update f a v ∘ ⇑g = function.update (f ∘ ⇑g) (⇑(g.symm) a) v
source
theorem function.update_apply_equiv_apply {α : Sort u_1} {β : Sort u_2} {α' : Sort u_3} [decidable_eq α'] [decidable_eq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) (a' : α') :
function.update f a v (⇑g a') = function.update (f ∘ ⇑g) (⇑(g.symm) a) v a'