mathlib documentation

data.equiv.basic

Equivalence between types

In this file we define two types:

Then we define

Tags

equivalence, congruence, bijective map

@[nolint]
structure equiv  :
Sort u_1Sort u_2Sort (max 1 (imax u_1 u_2) (imax u_2 u_1))

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

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

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

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

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

Equations
@[instance]
def equiv.has_coe_to_fun {α : Sort u} {β : Sort v} :

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

theorem equiv.injective_coe_fn {α : Sort u} {β : Sort v} :
function.injective (λ (e : α β) (x : α), e x)

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

@[simp]
theorem equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ e₂ : α β} :
e₁ = e₂ e₁ = e₂

@[ext]
theorem equiv.ext {α : Sort u} {β : Sort v} {f g : α β} :
(∀ (x : α), f x = g x)f = g

@[ext]
theorem equiv.perm.ext {α : Sort u} {σ τ : equiv.perm α} :
(∀ (x : α), σ x = τ x)σ = τ

theorem equiv.ext_iff {α : Sort u} {β : Sort v} {f g : α β} :
f = g ∀ (x : α), f x = g x

theorem equiv.perm.ext_iff {α : Sort u} {σ τ : equiv.perm α} :
σ = τ ∀ (x : α), σ x = τ x

def equiv.refl (α : Sort u_1) :
α α

Any type is equivalent to itself.

Equations
@[instance]
def equiv.inhabited' {α : Sort u} :
inhabited α)

Equations
def equiv.symm {α : Sort u} {β : Sort v} :
α ββ α

Inverse of an equivalence e : α ≃ β.

Equations
def equiv.simps.inv_fun {α : Sort u} {β : Sort v} :
α ββ → α

See Note [custom simps projection]

Equations
def equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} :
α ββ γα γ

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

Equations
@[simp]
theorem equiv.to_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.inv_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :

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

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

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

@[simp]
theorem equiv.range_eq_univ {α : Type u_1} {β : Type u_2} (e : α β) :

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

def equiv.decidable_eq {α : Sort u} {β : Sort v} (e : α β) [decidable_eq β] :

Transfer decidable_eq across an equivalence.

Equations
theorem equiv.nonempty_iff_nonempty {α : Sort u} {β : Sort v} :
α β(nonempty α nonempty β)

def equiv.inhabited {α : Sort u} {β : Sort v} [inhabited β] :
α βinhabited α

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

Equations
def equiv.unique {α : Sort u} {β : Sort v} [unique β] :
α βunique α

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

Equations
def equiv.cast {α β : Sort u_1} :
α = βα β

Equivalence between equal types.

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

@[simp]
theorem equiv.coe_refl {α : Sort u} :

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

@[simp]
theorem equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) :
(f.trans g) = g f

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

@[simp]
theorem equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α β) (x : β) :
e ((e.symm) x) = x

@[simp]
theorem equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
(e.symm) (e x) = x

@[simp]
theorem equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α β) :

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

@[simp]
theorem equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α β) {x y : α} :
f x = f y x = y

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

@[simp]
theorem equiv.cast_apply {α β : Sort u_1} (h : α = β) (x : α) :
(equiv.cast h) x = cast h x

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

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

@[simp]
theorem equiv.symm_symm {α : Sort u} {β : Sort v} (e : α β) :
e.symm.symm = e

@[simp]
theorem equiv.trans_refl {α : Sort u} {β : Sort v} (e : α β) :
e.trans (equiv.refl β) = e

@[simp]
theorem equiv.refl_symm {α : Sort u} :

@[simp]
theorem equiv.refl_trans {α : Sort u} {β : Sort v} (e : α β) :
(equiv.refl α).trans e = e

@[simp]
theorem equiv.symm_trans {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.trans_symm {α : Sort u} {β : Sort v} (e : α β) :

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

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

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

def equiv.equiv_congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} :
α βγ δα γ δ)

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

Equations
def equiv.perm_congr {α : Type u_1} {β : Type u_2} :
α βequiv.perm α equiv.perm β

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

Equations
theorem equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) :
e '' s = (e.symm) ⁻¹' s

theorem equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) (t : set β) :
t e '' s (e.symm) '' t s

theorem equiv.symm_image_image {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
(f.symm) '' (f '' s) = s

theorem equiv.image_compl {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
f '' s = (f '' s)

The group of permutations (self-equivalences) of a type α

@[instance]
def equiv.perm.perm_group {α : Type u} :

Equations
theorem equiv.perm.mul_apply {α : Type u} (f g : equiv.perm α) (x : α) :
(f * g) x = f (g x)

@[simp]
theorem equiv.perm.one_apply {α : Type u} (x : α) :
1 x = x

@[simp]
theorem equiv.perm.inv_apply_self {α : Type u} (f : equiv.perm α) (x : α) :
f⁻¹ (f x) = x

@[simp]
theorem equiv.perm.apply_inv_self {α : Type u} (f : equiv.perm α) (x : α) :
f (f⁻¹ x) = x

theorem equiv.perm.one_def {α : Type u} :

theorem equiv.perm.mul_def {α : Type u} (f g : equiv.perm α) :
f * g = equiv.trans g f

theorem equiv.perm.inv_def {α : Type u} (f : equiv.perm α) :

@[simp]
theorem equiv.perm.coe_mul {α : Type u} (f g : equiv.perm α) :
f * g = f g

def equiv.equiv_empty {α : Sort u} :
(α → false)α empty

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

Equations
def equiv.equiv_pempty {α : Sort v'} :
(α → false)α pempty

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

Equations

empty is equivalent to pempty.

Equations

pempty types from any two universes are equivalent.

Equations
def equiv.empty_of_not_nonempty {α : Sort u_1} :
¬nonempty αα empty

If α is not nonempty, then it is equivalent to empty.

Equations
def equiv.pempty_of_not_nonempty {α : Sort u_1} :

If α is not nonempty, then it is equivalent to pempty.

Equations
def equiv.prop_equiv_punit {p : Prop} :
p → p punit

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

Equations
@[simp]
theorem equiv.ulift_symm_apply {α : Type v} :
(equiv.ulift.symm) = ulift.up

def equiv.ulift {α : Type v} :
ulift α α

ulift α is equivalent to α.

Equations
@[simp]
theorem equiv.ulift_apply {α : Type v} :

@[simp]
theorem equiv.plift_apply {α : Sort u} :

def equiv.plift {α : Sort u} :
plift α α

plift α is equivalent to α.

Equations
@[simp]
theorem equiv.plift_symm_apply {α : Sort u} :
(equiv.plift.symm) = plift.up

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

equivalence of propositions is the same as iff

Equations
@[simp]
theorem equiv.arrow_congr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁ → β₁) (a : α₂) :
(e₁.arrow_congr e₂) f a = (e₂ f (e₁.symm)) a

def equiv.arrow_congr {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} :
α₁ α₂β₁ β₂(α₁ → β₁) (α₂ → β₂)

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

Equations
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

@[simp]
theorem equiv.arrow_congr_refl {α : Sort u_1} {β : Sort u_2} :

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

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

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

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
@[simp]
theorem equiv.arrow_congr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) (f : α₁ → β₁) (a : α₂) :
(hα.arrow_congr' hβ) f a = (f ((hα.symm) a))

@[simp]
theorem equiv.arrow_congr'_refl {α : Type u_1} {β : Type u_2} :

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

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

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

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

Equations
@[simp]
theorem equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : α → α) (a : β) :
(e.conj) f a = e (f ((e.symm) a))

@[simp]
theorem equiv.conj_refl {α : Sort u} :
(equiv.refl α).conj = equiv.refl (α → α)

@[simp]
theorem equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
(e₁.trans e₂).conj = e₁.conj.trans e₂.conj

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

theorem equiv.semiconj_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁) :

theorem equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) :

@[instance]
def equiv.is_associative {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [is_associative α₁ f] :

@[instance]
def equiv.is_idempotent {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [is_idempotent α₁ f] :

@[instance]
def equiv.is_left_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [is_left_cancel α₁ f] :

@[instance]
def equiv.is_right_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [is_right_cancel α₁ f] :

punit sorts in any two universes are equivalent.

Equations
def equiv.arrow_punit_equiv_punit (α : Sort u_1) :
(α → punit) punit

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

Equations
def equiv.punit_arrow_equiv (α : Sort u_1) :
(punit → α) α

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

Equations
def equiv.empty_arrow_equiv_punit (α : Sort u_1) :
(empty → α) punit

The sort of maps from empty is equivalent to punit.

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

The sort of maps from pempty is equivalent to punit.

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

The sort of maps from false is equivalent to punit.

Equations
def equiv.prod_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} :
α₁ α₂β₁ β₂α₁ × β₁ α₂ × β₂

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

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

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

def equiv.prod_comm (α : Type u_1) (β : Type u_2) :
α × β β × α

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

Equations
@[simp]
theorem equiv.prod_comm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :

@[simp]
theorem equiv.prod_comm_symm (α : Type u_1) (β : Type u_2) :

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

def equiv.prod_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
× β) × γ α × β × γ

Type product is associative up to an equivalence.

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

theorem equiv.prod_assoc_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {u : set γ} :
(equiv.prod_assoc α β γ) ⁻¹' s.prod (t.prod u) = (s.prod t).prod u

def equiv.prod_punit (α : Type u_1) :
α × punit α

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

Equations
@[simp]
theorem equiv.prod_punit_apply (α : Type u_1) (p : α × punit) :

def equiv.punit_prod (α : Type u_1) :
punit × α α

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

Equations
@[simp]
theorem equiv.punit_prod_apply (α : Type u_1) (a : punit × α) :

def equiv.prod_empty (α : Type u_1) :

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

Equations
def equiv.empty_prod (α : Type u_1) :

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

Equations
def equiv.prod_pempty (α : Type u_1) :

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

Equations
def equiv.pempty_prod (α : Type u_1) :

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

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

psum is equivalent to sum.

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

def equiv.sum_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} :
α₁ α₂β₁ β₂α₁ β₁ α₂ β₂

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

Equations
@[simp]
theorem equiv.sum_congr_symm {α β γ δ : Type u} (e : α β) (f : γ δ) :

bool is equivalent the sum of two punits.

Equations

Prop is noncomputably equivalent to bool.

Equations
@[simp]
theorem equiv.sum_comm_apply (α : Type u_1) (β : Type u_2) (a : α β) :

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

Sum of types is commutative up to an equivalence.

Equations
@[simp]
theorem equiv.sum_comm_symm (α : Type u_1) (β : Type u_2) :

def equiv.sum_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β) γ α β γ

Sum of types is associative up to an equivalence.

Equations
@[simp]
theorem equiv.sum_assoc_apply_in1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :

@[simp]
theorem equiv.sum_assoc_apply_in2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :

@[simp]
theorem equiv.sum_assoc_apply_in3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :

def equiv.sum_empty (α : Type u_1) :
α empty α

Sum with empty is equivalent to the original type.

Equations
@[simp]
theorem equiv.sum_empty_apply_inl {α : Type u_1} (a : α) :

def equiv.empty_sum (α : Type u_1) :
empty α α

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

Equations
@[simp]
theorem equiv.empty_sum_apply_inr {α : Type u_1} (a : α) :

def equiv.sum_pempty (α : Type u_1) :
α pempty α

Sum with pempty is equivalent to the original type.

Equations
@[simp]
theorem equiv.sum_pempty_apply_inl {α : Type u_1} (a : α) :

def equiv.pempty_sum (α : Type u_1) :
pempty α α

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

Equations
@[simp]
theorem equiv.pempty_sum_apply_inr {α : Type u_1} (a : α) :

def equiv.option_equiv_sum_punit (α : Type u_1) :

option α is equivalent to α ⊕ punit

Equations
@[simp]
theorem equiv.option_equiv_sum_punit_some {α : Type u_1} (a : α) :

@[simp]
theorem equiv.option_equiv_sum_punit_coe {α : Type u_1} (a : α) :

@[simp]

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
def equiv.sum_equiv_sigma_bool (α β : Type u_1) :
α β Σ (b : bool), cond b α β

α ⊕ β is equivalent to a sigma-type over bool.

Equations
@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :

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
@[simp]
theorem equiv.sigma_preimage_equiv_apply {α : Type u_1} {β : Type u_2} (f : α → β) (x : Σ (y : β), {x // f x = y}) :

@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :

def equiv.set_prod_equiv_sigma {α : Type u_1} {β : Type u_2} (s : set × β)) :
s Σ (x : α), {y : β | (x, y) s}

A set s in α × β is equivalent to the sigma-type Σ x, {y | (x, y) ∈ s}.

Equations
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 α.

Equations
@[simp]
theorem equiv.sum_compl_apply_inl {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : {a // p a}) :

@[simp]
theorem equiv.sum_compl_apply_inr {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : {a // ¬p a}) :

@[simp]
theorem equiv.sum_compl_apply_symm_of_pos {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) (h : p a) :

@[simp]
theorem equiv.sum_compl_apply_symm_of_neg {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) (h : ¬p a) :

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

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

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

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⟩

def equiv.fun_unique (α : Sort u) (β : Sort v) [unique α] :
(α → β) β

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

Equations
@[simp]
theorem equiv.fun_unique_symm_apply (α : Sort u) (β : Sort v) [unique α] (b : β) (a : α) :
((equiv.fun_unique α β).symm) b a = b

@[simp]
theorem equiv.fun_unique_apply (α : Sort u) (β : Sort v) [unique α] (f : α → β) :
(equiv.fun_unique α β) f = f (default α)

def equiv.Pi_congr_right {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} :
(Π (a : α), β₁ a β₂ a)((Π (a : α), β₁ a) Π (a : α), β₂ a)

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

Equations
def equiv.Pi_curry {α : Type u_1} {β : α → Type u_2} (γ : Π (a : α), β aSort 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).

Equations
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
@[simp]
theorem equiv.psigma_equiv_sigma_symm_apply {α : Type u_1} (β : α → Type u_2) (a : Σ (i : α), β i) :

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

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

def equiv.sigma_congr_right {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} :
(Π (a : α), β₁ a β₂ a)((Σ (a : α), β₁ a) Σ (a : α), β₂ a)

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

Equations
@[simp]
theorem equiv.sigma_congr_right_symm_apply {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ (a : α), β₂ a) :

@[simp]
theorem equiv.sigma_congr_left_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ α₂) (a : Σ (a : α₁), β (e a)) :

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
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
def equiv.sigma_congr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (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
def equiv.sigma_equiv_prod (α : Type u_1) (β : Type u_2) :
(Σ (_x : α), β) α × β

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

Equations
@[simp]
theorem equiv.sigma_equiv_prod_apply (α : Type u_1) (β : Type u_2) (a : Σ (_x : α), β) :

@[simp]
theorem equiv.sigma_equiv_prod_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :

def equiv.sigma_equiv_prod_of_equiv {α : Type u_1} {β : Type u_2} {β₁ : α → Type u_3} :
(Π (a : α), β₁ a β)sigma β₁ α × β

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

Equations
def equiv.prod_congr_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} :
(α₁ → β₁ β₂)β₁ × α₁ β₂ × α₁

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

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

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)

def equiv.prod_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} :
(α₁ → β₁ β₂)α₁ × β₁ α₁ × β₂

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

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

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)

@[simp]
theorem equiv.prod_congr_left_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :

@[simp]
theorem equiv.prod_congr_right_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :

theorem equiv.sigma_congr_right_sigma_equiv_prod {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :

theorem equiv.sigma_equiv_prod_sigma_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :

def equiv.perm.prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] :
α₁ → 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
@[simp]
theorem equiv.perm.prod_extend_right_apply_eq {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (b : β₁) :

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)

theorem equiv.perm.eq_of_prod_extend_right_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] {e : equiv.perm β₁} {a a' : α₁} {b : β₁} :
(equiv.perm.prod_extend_right a e) (a', b) (a', b)a' = a

@[simp]
theorem equiv.perm.fst_prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (ab : α₁ × β₁) :

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
def equiv.arrow_arrow_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α → β → γ) × β → γ)

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

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

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

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

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

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
@[simp]
theorem equiv.bool_to_equiv_prod_apply {α : Type u} (f : bool → α) :

@[simp]
theorem equiv.bool_to_equiv_prod_symm_apply_ff {α : Type u} (p : α × α) :

@[simp]
theorem equiv.bool_to_equiv_prod_symm_apply_tt {α : Type u} (p : α × α) :

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

Equations

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

Equations
def equiv.list_equiv_of_equiv {α : Type u_1} {β : Type u_2} :
α βlist α list β

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

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

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

Equations
def equiv.unique_congr {α : Sort u} {β : Sort v} :
α βunique α unique β

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

Equations
def equiv.subtype_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) :
(∀ (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}.

Equations
@[simp]
theorem equiv.subtype_congr_apply {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) (h : ∀ (a : α), p a q (e a)) (x : {x // p x}) :
(e.subtype_congr h) x = e x, _⟩

@[simp]
theorem equiv.subtype_congr_symm_apply {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) (h : ∀ (a : α), p a q (e a)) (y : {y // q y}) :
((e.subtype_congr h).symm) y = (e.symm) y, _⟩

@[simp]
theorem equiv.subtype_congr_right_symm_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x q x) (y : {b // (λ (x : α), q x) b}) :

@[simp]
theorem equiv.subtype_congr_right_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x q x) (x : {a // (λ (x : α), p x) a}) :

def equiv.subtype_congr_right {α : Sort u} {p q : α → Prop} :
(∀ (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
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
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
def equiv.subtype_congr_prop {α : Type u_1} {p q : α → Prop} :
p = qsubtype p subtype q

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

Equations
def equiv.set_congr {α : Type u_1} {s t : set α} :
s = ts t

The subtypes corresponding to equal sets are equivalent.

Equations
@[simp]
theorem equiv.set_congr_apply {α : Type u_1} {s t : set α} (h : s = t) (x : {a // (λ (a : α), (λ (x : α), x s) a) a}) :

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
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
def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} :
(∀ {x : α}, q xp 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
def equiv.subtype_univ_equiv {α : Type u} {p : α → Prop} :
(∀ (x : α), p x)subtype p α

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

Equations
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
def equiv.sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop) :
(∀ (x : α), p xq 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
def equiv.sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop) :
(∀ (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
def equiv.sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β) {p : α → Prop} {q : β → Prop} :
(∀ (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
def equiv.pi_equiv_subtype_sigma (ι : Type u_1) (π : ι → Type u_2) :
(Π (i : ι), «π» i) {f : ι → (Σ (i : ι), «π» i) | ∀ (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
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
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
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
@[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

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

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), _⟩

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

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

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

@[simp]
theorem equiv.set.univ_symm_apply (α : Type u_1) (a : α) :

def equiv.set.univ (α : Type u_1) :

univ α is equivalent to α.

Equations
@[simp]
theorem equiv.set.univ_apply (α : Type u_1) (a : set.univ) :

def equiv.set.empty (α : Type u_1) :

An empty set is equivalent to the empty type.

Equations
def equiv.set.pempty (α : Type u_1) :

An empty set is equivalent to a pempty type.

Equations
def equiv.set.union' {α : Type u_1} {s t : set α} (p : α → Prop) [decidable_pred p] :
(∀ (x : α), x sp x)(∀ (x : α), x t¬p x)(s t) s t

If sets s and t are separated by a decidable predicate, then s ∪ t is equivalent to s ⊕ t.

Equations
def equiv.set.union {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] :
s t (s t) s t

If sets s and t are disjoint, then s ∪ t is equivalent to s ⊕ t.

Equations
theorem equiv.set.union_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) {a : (s t)} (ha : a s) :

theorem equiv.set.union_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) {a : (s t)} (ha : a t) :

@[simp]
theorem equiv.set.union_symm_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) (a : s) :

@[simp]
theorem equiv.set.union_symm_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) (a : t) :

def equiv.set.singleton {α : Type u_1} (a : α) :

A singleton set is equivalent to a punit type.

Equations
@[simp]
theorem equiv.set.of_eq_apply {α : Type u} {s t : set α} (h : s = t) (x : s) :

def equiv.set.of_eq {α : Type u} {s t : set α} :
s = ts t

Equal sets are equivalent.

Equations
@[simp]
theorem equiv.set.of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (x : t) :

def equiv.set.insert {α : Type u} {s : set α} [decidable_pred s] {a : α} :
a s(insert a s) s punit

If a ∉ s, then insert a s is equivalent to s ⊕ punit.

Equations
@[simp]
theorem equiv.set.insert_symm_apply_inl {α : Type u} {s : set α} [decidable_pred s] {a : α} (H : a s) (b : s) :

@[simp]
theorem equiv.set.insert_symm_apply_inr {α : Type u} {s : set α} [decidable_pred s] {a : α} (H : a s) (b : punit) :

@[simp]
theorem equiv.set.insert_apply_left {α : Type u} {s : set α} [decidable_pred s] {a : α} (H : a s) :

@[simp]
theorem equiv.set.insert_apply_right {α : Type u} {s : set α} [decidable_pred s] {a : α} (H : a s) (b : s) :

def equiv.set.sum_compl {α : Type u_1} (s : set α) [decidable_pred s] :

If s : set α is a set with decidable membership, then s ⊕ sᶜ is equivalent to α.

Equations
@[simp]
theorem equiv.set.sum_compl_apply_inl {α : Type u} (s : set α) [decidable_pred s] (x : s) :

@[simp]
theorem equiv.set.sum_compl_apply_inr {α : Type u} (s : set α) [decidable_pred s] (x : s) :

theorem equiv.set.sum_compl_symm_apply_of_mem {α : Type u} {s : set α} [decidable_pred s] {x : α} (hx : x s) :

theorem equiv.set.sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred s] {x : α} (hx : x s) :

@[simp]
theorem equiv.set.sum_compl_symm_apply {α : Type u_1} {s : set α} [decidable_pred s] {x : s} :

@[simp]
theorem equiv.set.sum_compl_symm_apply_compl {α : Type u_1} {s : set α} [decidable_pred s] {x : s} :

def equiv.set.sum_diff_subset {α : Type u_1} {s t : set α} (h : s t) [decidable_pred s] :
s (t \ s) t

sum_diff_subset s t is the natural equivalence between s ⊕ (t \ s) and t, where s and t are two sets.

Equations
@[simp]
theorem equiv.set.sum_diff_subset_apply_inl {α : Type u_1} {s t : set α} (h : s t) [decidable_pred s] (x : s) :

@[simp]
theorem equiv.set.sum_diff_subset_apply_inr {α : Type u_1} {s t : set α} (h : s t) [decidable_pred s] (x : (t \ s)) :

theorem equiv.set.sum_diff_subset_symm_apply_of_mem {α : Type u_1} {s t : set α} (h : s t) [decidable_pred s] {x : t} (hx : x.val s) :

theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem {α : Type u_1} {s t : set α} (h : s t) [decidable_pred s] {x : t} (hx : x.val s) :

def equiv.set.union_sum_inter {α : Type u} (s t : set α) [decidable_pred s] :
(s t) (s t) s t

If s is a set with decidable membership, then the sum of s ∪ t and s ∩ t is equivalent to s ⊕ t.

Equations
def equiv.set.compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_pred s] [decidable_pred t] (e₀ : s t) :
{e // ∀ (x : s), e x = (e₀ x)} (s t)

Given an equivalence e₀ between sets s : set α and t : set β, the set of equivalences e : α ≃ β such that e ↑x = ↑(e₀ x) for each x : s is equivalent to the set of equivalences between sᶜ and tᶜ.

Equations
def equiv.set.prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
(s.prod t) s × t

The set product of two sets is equivalent to the type product of their coercions to types.

Equations
def equiv.set.image_of_inj_on {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
set.inj_on f ss (f '' s)

If a function f is injective on a set s, then s is equivalent to f '' s.

Equations
def equiv.set.image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :

If f is an injective function, then s is equivalent to f '' s.

Equations
@[simp]
theorem equiv.set.image_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : function.injective f) (p : s) :
(equiv.set.image f s H) p = f p, _⟩

theorem equiv.set.image_symm_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (u s : set α) :
(λ (x : (f '' s)), (((equiv.set.image f s hf).symm) x)) ⁻¹' u = coe ⁻¹' (f '' u)

def equiv.set.range {α : Sort u_1} {β : Type u_2} (f : α → β) :

If f : α → β is an injective function, then α is equivalent to the range of f.

Equations
@[simp]
theorem equiv.set.range_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (H : function.injective f) (x : α) :
(equiv.set.range f H) x = f x, _⟩

theorem equiv.set.apply_range_symm {α : Sort u_1} {β : Type u_2} (f : α → β) (H : function.injective f) (b : (set.range f)) :
f (((equiv.set.range f H).symm) b) = b

def equiv.set.congr {α : Type u_1} {β : Type u_2} :
α βset α set β

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

Equations
def equiv.set.sep {α : Type u} (s : set α) (t : α → Prop) :
{x ∈ s | t x} {x : s | t x}

The set {x ∈ s | t x} is equivalent to the set of x : s such that t x.

Equations
def equiv.set.powerset {α : Type u_1} (S : set α) :

The set 𝒫 S := {x | x ⊆ S} is equivalent to the type set S.

Equations
def equiv.of_bijective {α : Sort u_1} {β : Type u_2} (f : α → β) :

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

Equations
@[simp]
theorem equiv.of_bijective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.bijective f) (a : α) :

@[simp]
theorem equiv.of_injective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (a : α) :
(equiv.of_injective f hf) a = f a, _⟩

def equiv.of_injective {α : Sort u_1} {β : Type u_2} (f : α → β) :

If f is an injective function, then its domain is equivalent to its range.

Equations
def equiv.subtype_quotient_equiv_quotient_subtype {α : Sort u} (p₁ : α → Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) :
(∀ (a : α), p₁ a p₂ a)(∀ (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
def equiv.swap_core {α : Sort u} [decidable_eq α] :
α → α → α → α

A helper function for equiv.swap.

Equations
theorem equiv.swap_core_self {α : Sort u} [decidable_eq α] (r a : α) :

theorem equiv.swap_core_swap_core {α : Sort u} [decidable_eq α] (r a b : α) :

theorem equiv.swap_core_comm {α : Sort u} [decidable_eq α] (r a b : α) :

def equiv.swap {α : Sort u} [decidable_eq α] :
α → α → equiv.perm α

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

Equations
theorem equiv.swap_self {α : Sort u} [decidable_eq α] (a : α) :

theorem equiv.swap_comm {α : Sort u} [decidable_eq α] (a b : α) :

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)

@[simp]
theorem equiv.swap_apply_left {α : Sort u} [decidable_eq α] (a b : α) :
(equiv.swap a b) a = b

@[simp]
theorem equiv.swap_apply_right {α : Sort u} [decidable_eq α] (a b : α) :
(equiv.swap a b) b = a

theorem equiv.swap_apply_of_ne_of_ne {α : Sort u} [decidable_eq α] {a b x : α} :
x ax b(equiv.swap a b) x = x

@[simp]
theorem equiv.swap_swap {α : Sort u} [decidable_eq α] (a b : α) :

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

@[simp]
theorem equiv.swap_inv {α : Type u_1} [decidable_eq α] (x y : α) :

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

@[simp]
theorem equiv.swap_mul_self {α : Type u_1} [decidable_eq α] (i j : α) :
(equiv.swap i j) * equiv.swap i j = 1

@[simp]
theorem equiv.swap_apply_self {α : Type u_1} [decidable_eq α] (i j a : α) :
(equiv.swap i j) ((equiv.swap i j) a) = a

def equiv.set_value {α : Sort u} {β : Sort v} [decidable_eq α] :
α βα → β → α β

Augment an equivalence with a prescribed mapping f a = b

Equations
@[simp]
theorem equiv.set_value_eq {α : Sort u} {β : Sort v} [decidable_eq α] (f : α β) (a : α) (b : β) :
(f.set_value a b) a = b

theorem equiv.forall_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (f : α β) :
(∀ {x : α}, p x q (f x))((∀ (x : α), p x) ∀ (y : β), q y)

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

theorem equiv.forall₂_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) :
(∀ {x : α₁} {y : β₁}, p x y q (eα x) (eβ y))((∀ (x : α₁) (y : β₁), p x y) ∀ (x : α₂) (y : β₂), q x y)

theorem equiv.forall₂_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) :
(∀ {x : α₂} {y : β₂}, p ((eα.symm) x) ((eβ.symm) y) q x y)((∀ (x : α₁) (y : β₁), p x y) ∀ (x : α₂) (y : β₂), q x y)

theorem equiv.forall₃_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) :
(∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z q (eα x) (eβ y) (eγ z))((∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z)

theorem equiv.forall₃_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) :
(∀ {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)

theorem equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : α → Prop} (f : α β) :
(∀ (x : α), p x) ∀ (y : β), p ((f.symm) y)

theorem equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : β → Prop} (f : α β) :
(∀ (x : α), p (f x)) ∀ (y : β), p y

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

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

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
def equiv.Pi_congr {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (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
def equiv.Pi_congr' {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (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
@[instance]
def ulift.subsingleton {α : Type u_1} [subsingleton α] :

@[instance]
def plift.subsingleton {α : Sort u_1} [subsingleton α] :

@[instance]
def ulift.decidable_eq {α : Type u_1} [decidable_eq α] :

Equations
@[instance]
def plift.decidable_eq {α : Sort u_1} [decidable_eq α] :

Equations
def equiv_of_unique_of_unique {α : Sort u} {β : Sort v} [unique α] [unique β] :
α β

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

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

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

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

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

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

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

Equations
def unique_unique_equiv {α : Sort u} :

unique (unique α) is equivalent to unique α.

Equations
def quot.congr {α : Sort u} {β : Sort v} {ra : α → α → Prop} {rb : β → β → Prop} (e : α β) :
(∀ (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
def quot.congr_right {α : Sort u} {r r' : α → α → Prop} :
(∀ (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
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
def quotient.congr {α : Sort u} {β : Sort v} {ra : setoid α} {rb : setoid β} (e : α β) :
(∀ (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
def quotient.congr_right {α : Sort u} {r r' : setoid α} :
(∀ (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
def set.bij_on.equiv {α : Type u_1} {β : Type u_2} {s : set β} (f : α → β) :

If a function is a bijection between univ and a set s in the target type, it induces an equivalence between the original type and the type ↑s.

Equations
theorem dite_comp_equiv_update {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} (e : β s) (v : β → γ) (w : α → γ) (j : β) (x : γ) [decidable_eq β] [decidable_eq α] [Π (j : α), decidable (j s)] :
(λ (i : α), dite (i s) (λ (h : i s), function.update v j x ((e.symm) i, h⟩)) (λ (h : i s), w i)) = function.update (λ (i : α), dite (i s) (λ (h : i s), v ((e.symm) i, h⟩)) (λ (h : i s), w i)) (e j) x

The composition of an updated function with an equiv on a subset can be expressed as an updated function.