mathlib docs: data.equiv.basic

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

⇑(e₁.arrow_congr e₂) f x = ⇑e₂ (f (⇑(e₁.symm) x))

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

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

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

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

Equations

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

source

@[simp]

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

⇑(e₁.arrow_congr' e₂) f x = ⇑e₂ (f (⇑(e₁.symm) x))

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

α ≃ β → (α → α) ≃ (β → β)

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

Equations

e.conj = e.arrow_congr e

source

@[simp]

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

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

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

def equiv.punit_equiv_punit :

punit ≃ punit

punit sorts in any two universes are equivalent.

Equations

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

source

def equiv.arrow_punit_equiv_punit (α : Sort u_1) :

(α → punit) ≃ punit

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

Equations

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

source

def equiv.punit_arrow_equiv (α : Sort u_1) :

(punit → α) ≃ α

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

Equations

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

source

def equiv.empty_arrow_equiv_punit (α : Sort u_1) :

(empty → α) ≃ punit

The sort of maps from empty is equivalent to punit.

Equations

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

source

def equiv.pempty_arrow_equiv_punit (α : Sort u_1) :

(pempty → α) ≃ punit

The sort of maps from pempty is equivalent to punit.

Equations

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

source

def equiv.false_arrow_equiv_punit (α : Sort u_1) :

(false → α) ≃ punit

The sort of maps from false is equivalent to punit.

Equations

equiv.false_arrow_equiv_punit α = (equiv.false_equiv_empty.arrow_congr (equiv.refl α)).trans (equiv.empty_arrow_equiv_punit α)

source

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

α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂

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

Equations

e₁.prod_congr e₂ = {to_fun := prod.map ⇑e₁ ⇑e₂, inv_fun := prod.map ⇑(e₁.symm) ⇑(e₂.symm), left_inv := _, right_inv := _}

source

@[simp]

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

⇑(e₁.prod_congr e₂) = prod.map ⇑e₁ ⇑e₂

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

equiv.prod_comm α β = {to_fun := prod.swap β, inv_fun := prod.swap α, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.coe_prod_comm (α : Type u_1) (β : Type u_2) :

⇑(equiv.prod_comm α β) = prod.swap

source

@[simp]

theorem equiv.prod_comm_symm (α : Type u_1) (β : Type u_2) :

(equiv.prod_comm α β).symm = equiv.prod_comm β α

source

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

(α × β) × γ ≃ α × β × γ

Type product is associative up to an equivalence.

Equations

equiv.prod_assoc α β γ = {to_fun := λ (p : (α × β) × γ), (p.fst.fst, p.fst.snd, p.snd), inv_fun := λ (p : α × β × γ), ((p.fst, p.snd.fst), p.snd.snd), left_inv := _, right_inv := _}

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.prod_assoc_sym_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_punit (α : Type u_1) :

α × punit ≃ α

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

Equations

equiv.prod_punit α = {to_fun := λ (p : α × punit), p.fst, inv_fun := λ (a : α), (a, punit.star), left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.prod_punit_apply {α : Type u_1} (a : α × punit) :

⇑(equiv.prod_punit α) a = a.fst

source

def equiv.punit_prod (α : Type u_1) :

punit × α ≃ α

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

Equations

equiv.punit_prod α = (equiv.prod_comm punit α).trans (equiv.prod_punit α)

source

@[simp]

theorem equiv.punit_prod_apply {α : Type u_1} (a : punit × α) :

⇑(equiv.punit_prod α) a = a.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

equiv.prod_empty α = equiv.equiv_empty _

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

equiv.empty_prod α = equiv.equiv_empty _

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

equiv.prod_pempty α = equiv.equiv_pempty _

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

equiv.pempty_prod α = equiv.equiv_pempty _

source

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

psum α β ≃ α ⊕ β

psum is equivalent to sum.

Equations

equiv.psum_equiv_sum α β = {to_fun := λ (s : psum α β), s.cases_on sum.inl sum.inr, inv_fun := λ (s : α ⊕ β), s.cases_on psum.inl psum.inr, left_inv := _, right_inv := _}

source

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

α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂

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

Equations

ea.sum_congr eb = {to_fun := sum.map ⇑ea ⇑eb, inv_fun := sum.map ⇑(ea.symm) ⇑(eb.symm), left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sum_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (a : α₁ ⊕ β₁) :

⇑(e₁.sum_congr e₂) a = sum.map ⇑e₁ ⇑e₂ a

source

@[simp]

theorem equiv.sum_congr_symm {α β γ δ : Type u} (e : α ≃ β) (f : γ ≃ δ) :

(e.sum_congr f).symm = e.symm.sum_congr f.symm

source

def equiv.bool_equiv_punit_sum_punit :

bool ≃ punit ⊕ punit

bool is equivalent the sum of two punits.

Equations

equiv.bool_equiv_punit_sum_punit = {to_fun := λ (b : bool), cond b (sum.inr punit.star) (sum.inl punit.star), inv_fun := λ (s : punit ⊕ punit), s.rec_on (λ (_x : punit), bool.ff) (λ (_x : punit), bool.tt), left_inv := equiv.bool_equiv_punit_sum_punit._proof_1, right_inv := equiv.bool_equiv_punit_sum_punit._proof_2}

source

def equiv.Prop_equiv_bool :

Prop ≃ bool

Prop is noncomputably equivalent to bool.

Equations

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

source

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

α ⊕ β ≃ β ⊕ α

Sum of types is commutative up to an equivalence.

Equations

equiv.sum_comm α β = {to_fun := sum.swap β, inv_fun := sum.swap α, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sum_comm_apply (α : Type u_1) (β : Type u_2) (a : α ⊕ β) :

⇑(equiv.sum_comm α β) a = a.swap

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

equiv.sum_assoc α β γ = {to_fun := sum.elim (sum.elim sum.inl (sum.inr ∘ sum.inl)) (sum.inr ∘ sum.inr), inv_fun := sum.elim (sum.inl ∘ sum.inl) (sum.elim (sum.inl ∘ sum.inr) sum.inr), left_inv := _, right_inv := _}

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

α ⊕ empty ≃ α

Sum with empty is equivalent to the original type.

Equations

equiv.sum_empty α = {to_fun := sum.elim id (empty.rec (λ (n : empty), α)), inv_fun := sum.inl empty, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sum_empty_apply_inl {α : Type u_1} (a : α) :

⇑(equiv.sum_empty α) (sum.inl a) = a

source

def equiv.empty_sum (α : Type u_1) :

empty ⊕ α ≃ α

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

Equations

equiv.empty_sum α = (equiv.sum_comm empty α).trans (equiv.sum_empty α)

source

@[simp]

theorem equiv.empty_sum_apply_inr {α : Type u_1} (a : α) :

⇑(equiv.empty_sum α) (sum.inr a) = a

source

def equiv.sum_pempty (α : Type u_1) :

α ⊕ pempty ≃ α

Sum with pempty is equivalent to the original type.

Equations

equiv.sum_pempty α = {to_fun := sum.elim id (pempty.rec (λ (n : pempty), α)), inv_fun := sum.inl pempty, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.sum_pempty_apply_inl {α : Type u_1} (a : α) :

⇑(equiv.sum_pempty α) (sum.inl a) = a

source

def equiv.pempty_sum (α : Type u_1) :

pempty ⊕ α ≃ α

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

Equations

equiv.pempty_sum α = (equiv.sum_comm pempty α).trans (equiv.sum_pempty α)

source

@[simp]

theorem equiv.pempty_sum_apply_inr {α : Type u_1} (a : α) :

⇑(equiv.pempty_sum α) (sum.inr a) = a

source

def equiv.option_equiv_sum_punit (α : Type u_1) :

option α ≃ α ⊕ punit

option α is equivalent to α ⊕ punit

Equations

equiv.option_equiv_sum_punit α = {to_fun := λ (o : option α), equiv.option_equiv_sum_punit._match_1 α o, inv_fun := λ (s : α ⊕ punit), equiv.option_equiv_sum_punit._match_2 α s, left_inv := _, right_inv := _}
equiv.option_equiv_sum_punit._match_1 α (option.some a) = sum.inl a
equiv.option_equiv_sum_punit._match_1 α option.none = sum.inr punit.star
equiv.option_equiv_sum_punit._match_2 α (sum.inr _x) = option.none
equiv.option_equiv_sum_punit._match_2 α (sum.inl a) = option.some a

source

@[simp]

theorem equiv.option_equiv_sum_punit_none {α : Type u_1} :

⇑(equiv.option_equiv_sum_punit α) option.none = sum.inr ()

source

@[simp]

theorem equiv.option_equiv_sum_punit_some {α : Type u_1} (a : α) :

⇑(equiv.option_equiv_sum_punit α) (option.some a) = sum.inl a

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

equiv.option_is_some_equiv α = {to_fun := λ (o : {x // ↥(x.is_some)}), option.get _, inv_fun := λ (x : α), ⟨option.some x, _⟩, left_inv := _, right_inv := _}

source

def equiv.sum_equiv_sigma_bool (α β : Type u_1) :

α ⊕ β ≃ Σ (b : bool), cond b α β

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

Equations

equiv.sum_equiv_sigma_bool α β = {to_fun := λ (s : α ⊕ β), equiv.sum_equiv_sigma_bool._match_1 α β s, inv_fun := λ (s : Σ (b : bool), cond b α β), equiv.sum_equiv_sigma_bool._match_2 α β s, left_inv := _, right_inv := _}
equiv.sum_equiv_sigma_bool._match_1 α β (sum.inr b) = ⟨bool.ff, b⟩
equiv.sum_equiv_sigma_bool._match_1 α β (sum.inl a) = ⟨bool.tt, a⟩
equiv.sum_equiv_sigma_bool._match_2 α β ⟨bool.tt, a⟩ = sum.inl a
equiv.sum_equiv_sigma_bool._match_2 α β ⟨bool.ff, b⟩ = sum.inr b

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

equiv.sigma_preimage_equiv f = {to_fun := λ (x : Σ (y : β), {x // f x = y}), x.snd.val, inv_fun := λ (x : α), ⟨f x, ⟨x, _⟩⟩, left_inv := _, right_inv := _}

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.val

source

@[simp]

theorem equiv.sigma_preimage_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

(⇑((equiv.sigma_preimage_equiv f).symm) a).fst = f a

source

@[simp]

theorem equiv.sigma_preimage_equiv_symm_apply_snd_fst {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

(⇑((equiv.sigma_preimage_equiv f).symm) a).snd.val = a

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

Equations

equiv.sum_compl p = {to_fun := sum.elim coe coe, inv_fun := λ (a : α), dite (p a) (λ (h : p a), sum.inl ⟨a, h⟩) (λ (h : ¬p a), sum.inr ⟨a, h⟩), left_inv := _, right_inv := _}

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

equiv.subtype_preimage p x₀ = {to_fun := λ (x : {x // x ∘ coe = x₀}) (a : {a // ¬p a}), ↑x ↑a, inv_fun := λ (x : {a // ¬p a} → β), ⟨λ (a : α), dite (p a) (λ (h : p a), x₀ ⟨a, h⟩) (λ (h : ¬p a), x ⟨a, h⟩), _⟩, left_inv := _, right_inv := _}

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

⇑(equiv.subtype_preimage p x₀) x = λ (a : {a // ¬p a}), ↑x ↑a

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} → β) :

↑(⇑((equiv.subtype_preimage p x₀).symm) x) = λ (a : α), dite (p a) (λ (h : p a), x₀ ⟨a, h⟩) (λ (h : ¬p a), x ⟨a, h⟩)

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.fun_unique (α : Sort u) (β : Sort v) [unique α] :

(α → β) ≃ β

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

Equations

equiv.fun_unique α β = {to_fun := λ (f : α → β), f (inhabited.default α), inv_fun := λ (b : β) (a : α), b, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.fun_unique_apply {α : Sort u} {β : Sort v} [unique α] (f : α → β) :

⇑(equiv.fun_unique α β) f = f (inhabited.default α)

source

@[simp]

theorem equiv.fun_unique_symm_apply {α : Sort u} {β : Sort v} [unique α] (b : β) (a : α) :

⇑((equiv.fun_unique α β).symm) b a = b

source

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

equiv.Pi_congr_right F = {to_fun := λ (H : Π (a : α), β₁ a) (a : α), ⇑(F a) (H a), inv_fun := λ (H : Π (a : α), β₂ a) (a : α), ⇑((F a).symm) (H a), left_inv := _, right_inv := _}

source

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

equiv.Pi_curry γ = {to_fun := λ (f : Π (x : Σ (i : α), β i), γ x.fst x.snd) (x : α) (y : β x), f ⟨x, y⟩, inv_fun := λ (f : Π (a : α) (b : β a), γ a b) (x : Σ (i : α), β i), f x.fst x.snd, left_inv := _, right_inv := _}

source

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

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

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

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

equiv.sigma_congr_right F = {to_fun := λ (a : Σ (a : α), β₁ a), ⟨a.fst, ⇑(F a.fst) a.snd⟩, inv_fun := λ (a : Σ (a : α), β₂ a), ⟨a.fst, ⇑((F a.fst).symm) a.snd⟩, left_inv := _, right_inv := _}

source

@[simp]

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

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

source

@[simp]

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

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

source

def equiv.sigma_congr_left {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) :

(Σ (a : α₁), β (⇑e a)) ≃ Σ (a : α₂), β a

An equivalence f : α₁ ≃ α₂ generates an equivalence between Σ a, β (f a) and Σ a, β a.

Equations

e.sigma_congr_left = {to_fun := λ (a : Σ (a : α₁), β (⇑e a)), ⟨⇑e a.fst, a.snd⟩, inv_fun := λ (a : Σ (a : α₂), β a), ⟨⇑(e.symm) a.fst, eq.rec a.snd _⟩, left_inv := _, right_inv := _}

source

@[simp]

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

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

source

def equiv.sigma_congr_left' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ → Type u_3} (f : α₁ ≃ α₂) :

(Σ (a : α₁), β a) ≃ Σ (a : α₂), β (⇑(f.symm) a)

Transporting a sigma type through an equivalence of the base

Equations

f.sigma_congr_left' = f.symm.sigma_congr_left.symm

source

def equiv.sigma_congr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ ≃ α₂) :

(Π (a : α₁), β₁ a ≃ β₂ (⇑f a)) → sigma β₁ ≃ sigma β₂

Transporting a sigma type through an equivalence of the base and a family of equivalences of matching fibers

Equations

f.sigma_congr F = (equiv.sigma_congr_right F).trans f.sigma_congr_left

source

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

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

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

Equations

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

source

@[simp]

theorem equiv.sigma_equiv_prod_apply {α : Type u_1} {β : Type u_2} (x : Σ (_x : α), β) :

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

source

@[simp]

theorem equiv.sigma_equiv_prod_symm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :

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

source

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

equiv.sigma_equiv_prod_of_equiv F = (equiv.sigma_congr_right F).trans (equiv.sigma_equiv_prod α β)

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

equiv.arrow_prod_equiv_prod_arrow α β γ = {to_fun := λ (f : γ → α × β), (λ (c : γ), (f c).fst, λ (c : γ), (f c).snd), inv_fun := λ (p : (γ → α) × (γ → β)) (c : γ), (p.fst c, p.snd c), left_inv := _, right_inv := _}

source

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

(α → β → γ) ≃ (α × β → γ)

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

Equations

equiv.arrow_arrow_equiv_prod_arrow α β γ = {to_fun := function.uncurry γ, inv_fun := function.curry γ, left_inv := _, right_inv := _}

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

equiv.sum_arrow_equiv_prod_arrow α β γ = {to_fun := λ (f : α ⊕ β → γ), (f ∘ sum.inl, f ∘ sum.inr), inv_fun := λ (p : (α → γ) × (β → γ)), sum.elim p.fst p.snd, left_inv := _, right_inv := _}

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

equiv.sum_prod_distrib α β γ = {to_fun := λ (p : (α ⊕ β) × γ), equiv.sum_prod_distrib._match_1 α β γ p, inv_fun := λ (s : α × γ ⊕ β × γ), equiv.sum_prod_distrib._match_2 α β γ s, left_inv := _, right_inv := _}
equiv.sum_prod_distrib._match_1 α β γ (sum.inr b, c) = sum.inr (b, c)
equiv.sum_prod_distrib._match_1 α β γ (sum.inl a, c) = sum.inl (a, c)
equiv.sum_prod_distrib._match_2 α β γ (sum.inr q) = (sum.inr q.fst, q.snd)
equiv.sum_prod_distrib._match_2 α β γ (sum.inl q) = (sum.inl q.fst, q.snd)

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

equiv.prod_sum_distrib α β γ = ((equiv.prod_comm α (β ⊕ γ)).trans (equiv.sum_prod_distrib β γ α)).trans ((equiv.prod_comm β α).sum_congr (equiv.prod_comm γ α))

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

equiv.sigma_prod_distrib α β = {to_fun := λ (p : (Σ (i : ι), α i) × β), ⟨p.fst.fst, (p.fst.snd, p.snd)⟩, inv_fun := λ (p : Σ (i : ι), α i × β), (⟨p.fst, p.snd.fst⟩, p.snd.snd), left_inv := _, right_inv := _}

source

def equiv.bool_prod_equiv_sum (α : Type u) :

bool × α ≃ α ⊕ α

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

Equations

equiv.bool_prod_equiv_sum α = ((equiv.bool_equiv_punit_sum_punit.prod_congr (equiv.refl α)).trans (equiv.sum_prod_distrib unit unit α)).trans ((equiv.punit_prod α).sum_congr (equiv.punit_prod α))

source

def equiv.nat_equiv_nat_sum_punit :

ℕ ≃ ℕ ⊕ punit

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

Equations

equiv.nat_equiv_nat_sum_punit = {to_fun := λ (n : ℕ), equiv.nat_equiv_nat_sum_punit._match_1 n, inv_fun := λ (s : ℕ ⊕ punit), equiv.nat_equiv_nat_sum_punit._match_2 s, left_inv := equiv.nat_equiv_nat_sum_punit._proof_1, right_inv := equiv.nat_equiv_nat_sum_punit._proof_2}
equiv.nat_equiv_nat_sum_punit._match_1 a.succ = sum.inl a
equiv.nat_equiv_nat_sum_punit._match_1 0 = sum.inr punit.star
equiv.nat_equiv_nat_sum_punit._match_2 (sum.inr punit.star) = 0
equiv.nat_equiv_nat_sum_punit._match_2 (sum.inl n) = n.succ

source

def equiv.nat_sum_punit_equiv_nat :

ℕ ⊕ punit ≃ ℕ

ℕ ⊕ punit is equivalent to ℕ.

Equations

equiv.nat_sum_punit_equiv_nat = equiv.nat_equiv_nat_sum_punit.symm

source

def equiv.int_equiv_nat_sum_nat :

ℤ ≃ ℕ ⊕ ℕ

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

Equations

equiv.int_equiv_nat_sum_nat = {to_fun := λ (z : ℤ), z.cases_on (λ (z : ℕ), sum.inl z) (λ (z : ℕ), sum.inr z), inv_fun := λ (z : ℕ ⊕ ℕ), z.cases_on (λ (z : ℕ), int.of_nat z) (λ (z : ℕ), -[1+ z]), left_inv := equiv.int_equiv_nat_sum_nat._proof_1, right_inv := equiv.int_equiv_nat_sum_nat._proof_2}

source

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

e.list_equiv_of_equiv = {to_fun := list.map ⇑e, inv_fun := list.map ⇑(e.symm), left_inv := _, right_inv := _}

source

def equiv.fin_equiv_subtype (n : ℕ) :

fin n ≃ {m // m < n}

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

Equations

equiv.fin_equiv_subtype n = {to_fun := λ (x : fin n), ⟨x.val, _⟩, inv_fun := λ (x : {m // m < n}), ⟨x.val, _⟩, left_inv := _, right_inv := _}

source

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

α ≃ β → unique α ≃ unique β

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

Equations

e.unique_congr = {to_fun := λ (h : unique α), e.symm.unique, inv_fun := λ (h : unique β), e.unique, left_inv := _, right_inv := _}

source

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

e.subtype_congr h = {to_fun := λ (x : {a // p a}), ⟨⇑e x.val, _⟩, inv_fun := λ (y : {b // q b}), ⟨⇑(e.symm) y.val, _⟩, left_inv := _, right_inv := _}

source

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

equiv.subtype_congr_right e = (equiv.refl α).subtype_congr e

source

@[simp]

theorem equiv.subtype_congr_right_mk {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) {x : α} (h : p x) :

⇑(equiv.subtype_congr_right e) ⟨x, h⟩ = ⟨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

e.subtype_equiv_of_subtype = e.subtype_congr _

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

e.subtype_equiv_of_subtype' = e.symm.subtype_equiv_of_subtype.symm

source

def equiv.subtype_congr_prop {α : Type u_1} {p q : α → Prop} :

p = q → subtype p ≃ subtype q

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

Equations

equiv.subtype_congr_prop h = (equiv.refl α).subtype_congr _

source

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

s = t → ↥s ≃ ↥t

The subtypes corresponding to equal sets are equivalent.

Equations

equiv.set_congr h = equiv.subtype_congr_prop h

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

equiv.subtype_subtype_equiv_subtype_exists p q = {to_fun := λ (_x : subtype q), equiv.subtype_subtype_equiv_subtype_exists._match_1 p q _x, inv_fun := λ (_x : {a // ∃ (h : p a), q ⟨a, h⟩}), equiv.subtype_subtype_equiv_subtype_exists._match_2 p q _x, left_inv := _, right_inv := _}
equiv.subtype_subtype_equiv_subtype_exists._match_1 p q ⟨⟨a, ha⟩, ha'⟩ = ⟨a, _⟩
equiv.subtype_subtype_equiv_subtype_exists._match_2 p q ⟨a, ha⟩ = ⟨⟨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

equiv.subtype_subtype_equiv_subtype_inter p q = (equiv.subtype_subtype_equiv_subtype_exists p (λ (x : subtype p), q x.val)).trans (equiv.subtype_congr_right _)

source

def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} :

(∀ {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

equiv.subtype_subtype_equiv_subtype h = (equiv.subtype_subtype_equiv_subtype_inter p q).trans (equiv.subtype_congr_right _)

source

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

equiv.subtype_univ_equiv h = {to_fun := λ (x : subtype p), ↑x, inv_fun := λ (x : α), ⟨x, _⟩, left_inv := _, right_inv := _}

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

equiv.subtype_sigma_equiv p q = {to_fun := λ (x : {y // q y.fst}), ⟨⟨x.val.fst, _⟩, x.val.snd⟩, inv_fun := λ (x : Σ (x : subtype q), p x.val), ⟨⟨x.fst.val, x.snd⟩, _⟩, left_inv := _, right_inv := _}

source

def equiv.sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop) :

(∀ (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

equiv.sigma_subtype_equiv_of_subset p q h = (equiv.subtype_sigma_equiv p q).symm.trans (equiv.subtype_univ_equiv _)

source

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

equiv.sigma_subtype_preimage_equiv f p h = (equiv.sigma_subtype_equiv_of_subset (λ (y : β), {x // f x = y}) p _).trans (equiv.sigma_preimage_equiv f)

source

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

equiv.sigma_subtype_preimage_equiv_subtype f h = (equiv.sigma_congr_right (λ (y : subtype q), ((equiv.subtype_subtype_equiv_subtype_exists p (λ (x : subtype p), ⟨f ↑x, _⟩ = y)).trans (equiv.subtype_congr_right _)).symm)).trans (equiv.sigma_preimage_equiv (λ (x : subtype p), ⟨f ↑x, _⟩))

source

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

equiv.pi_equiv_subtype_sigma ι π = {to_fun := λ (f : Π (i : ι), π i), ⟨λ (i : ι), ⟨i, f i⟩, _⟩, inv_fun := λ (f : ↥{f : ι → (Σ (i : ι), π i) | ∀ (i : ι), (f i).fst = i}) (i : ι), _.mpr (f.val i).snd, left_inv := _, right_inv := _}

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

equiv.subtype_pi_equiv_pi = {to_fun := λ (f : {f // ∀ (a : α), p a (f a)}) (a : α), ⟨f.val a, _⟩, inv_fun := λ (f : Π (a : α), {b // p a b}), ⟨λ (a : α), (f a).val, _⟩, left_inv := _, right_inv := _}

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

equiv.subtype_prod_equiv_prod = {to_fun := λ (x : {c // p c.fst ∧ q c.snd}), (⟨x.val.fst, _⟩, ⟨x.val.snd, _⟩), inv_fun := λ (x : {a // p a} × {b // q b}), ⟨(x.fst.val, x.snd.val), _⟩, left_inv := _, right_inv := _}

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

equiv.subtype_equiv_codomain f = (equiv.subtype_preimage (λ (x' : X), x' ≠ x) f).trans (equiv.fun_unique {x' // ¬x' ≠ x} Y)

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

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

↥set.univ ≃ α

univ α is equivalent to α.

Equations

equiv.set.univ α = {to_fun := subtype.val (λ (x : α), x ∈ set.univ), inv_fun := λ (a : α), ⟨a, trivial⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.set.univ_apply {α : Type u} (x : ↥set.univ) :

⇑(equiv.set.univ α) x = ↑x

source

@[simp]

theorem equiv.set.univ_symm_apply {α : Type u} (x : α) :

⇑((equiv.set.univ α).symm) x = ⟨x, trivial⟩

source

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

↥∅ ≃ empty

An empty set is equivalent to the empty type.

Equations

equiv.set.empty α = equiv.equiv_empty _

source

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

↥∅ ≃ pempty

An empty set is equivalent to a pempty type.

Equations

equiv.set.pempty α = equiv.equiv_pempty _

source

def equiv.set.union' {α : Type u_1} {s t : set α} (p : α → Prop) [decidable_pred p] :

(∀ (x : α), x ∈ s → p 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

equiv.set.union' p hs ht = {to_fun := λ (x : ↥(s ∪ t)), dite (p ↑x) (λ (hp : p ↑x), sum.inl ⟨x.val, _⟩) (λ (hp : ¬p ↑x), sum.inr ⟨x.val, _⟩), inv_fun := λ (o : ↥s ⊕ ↥t), equiv.set.union'._match_1 o, left_inv := _, right_inv := _}
equiv.set.union'._match_1 (sum.inr x) = ⟨↑x, _⟩
equiv.set.union'._match_1 (sum.inl x) = ⟨↑x, _⟩

source

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

equiv.set.union H = equiv.set.union' (λ (x : α), x ∈ s) equiv.set.union._proof_1 _

source

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

⇑(equiv.set.union H) a = sum.inl ⟨↑a, ha⟩

source

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

⇑(equiv.set.union H) a = sum.inr ⟨↑a, ha⟩

source

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

↥{a} ≃ punit

A singleton set is equivalent to a punit type.

Equations

equiv.set.singleton a = {to_fun := λ (_x : ↥{a}), punit.star, inv_fun := λ (_x : punit), ⟨a, _⟩, left_inv := _, right_inv := _}

source

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

s = t → ↥s ≃ ↥t

Equal sets are equivalent.

Equations

equiv.set.of_eq h = {to_fun := λ (x : ↥s), ⟨x.val, _⟩, inv_fun := λ (x : ↥t), ⟨x.val, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.set.of_eq_apply {α : Type u} {s t : set α} (h : s = t) (a : ↥s) :

⇑(equiv.set.of_eq h) a = ⟨↑a, _⟩

source

@[simp]

theorem equiv.set.of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (a : ↥t) :

⇑((equiv.set.of_eq h).symm) a = ⟨↑a, _⟩

source

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

a ∉ s → ↥(has_insert.insert a s) ≃ ↥s ⊕ punit

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

Equations

equiv.set.insert H = ((equiv.set.of_eq equiv.set.insert._proof_1).trans (equiv.set.union _)).trans ((equiv.refl ↥s).sum_congr (equiv.set.singleton a))

source

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

↥s ⊕ ↥sᶜ ≃ α

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

Equations

equiv.set.sum_compl s = ((equiv.set.union _).symm.trans (equiv.set.of_eq _)).trans (equiv.set.univ α)

source

@[simp]

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

⇑(equiv.set.sum_compl s) (sum.inl x) = ↑x

source

@[simp]

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

⇑(equiv.set.sum_compl s) (sum.inr x) = ↑x

source

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

⇑((equiv.set.sum_compl s).symm) x = sum.inl ⟨x, hx⟩

source

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

⇑((equiv.set.sum_compl s).symm) x = sum.inr ⟨x, hx⟩

source

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

equiv.set.sum_diff_subset h = (equiv.set.union equiv.set.sum_diff_subset._proof_1).symm.trans (equiv.set.of_eq _)

source

@[simp]

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

⇑(equiv.set.sum_diff_subset h) (sum.inl x) = set.inclusion h x

source

@[simp]

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

⇑(equiv.set.sum_diff_subset h) (sum.inr x) = set.inclusion _ x

source

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

⇑((equiv.set.sum_diff_subset h).symm) x = sum.inl ⟨↑x, hx⟩

source

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

⇑((equiv.set.sum_diff_subset h).symm) x = sum.inr ⟨↑x, _⟩

source

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

equiv.set.union_sum_inter s t = ((((_.mpr (equiv.refl (↥(s ∪ t) ⊕ ↥(s ∩ t)))).trans ((equiv.set.union _).sum_congr (equiv.refl ↥(s ∩ t)))).trans (equiv.sum_assoc ↥s ↥(t \ s) ↥(s ∩ t))).trans ((equiv.refl ↥s).sum_congr (equiv.set.union' (λ (_x : α), _x ∉ s) _ _).symm)).trans (_.mpr (equiv.refl (↥s ⊕ ↥t)))

source

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

equiv.set.prod s t = equiv.subtype_prod_equiv_prod

source

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

set.inj_on f s → ↥s ≃ ↥(f '' s)

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

Equations

equiv.set.image_of_inj_on f s H = {to_fun := λ (p : ↥s), ⟨f ↑p, _⟩, inv_fun := λ (p : ↥(f '' s)), ⟨classical.some _, _⟩, left_inv := _, right_inv := _}

source

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

function.injective f → ↥s ≃ ↥(f '' s)

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

Equations

equiv.set.image f s H = equiv.set.image_of_inj_on f s _

source

@[simp]

theorem equiv.set.image_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : function.injective f) (a : α) (h : a ∈ s) :

⇑(equiv.set.image f s H) ⟨a, h⟩ = ⟨f a, _⟩

source

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)

source

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

function.injective f → α ≃ ↥(set.range f)

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

Equations

equiv.set.range f H = {to_fun := λ (x : α), ⟨f x, _⟩, inv_fun := λ (x : ↥(set.range f)), classical.some _, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.set.range_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (H : function.injective f) (a : α) :

⇑(equiv.set.range f H) a = ⟨f a, _⟩

source

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

source

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

α ≃ β → set α ≃ set β

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

Equations

equiv.set.congr e = {to_fun := λ (s : set α), ⇑e '' s, inv_fun := λ (t : set β), ⇑(e.symm) '' t, left_inv := _, right_inv := _}

source

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

equiv.set.sep s t = (equiv.subtype_subtype_equiv_subtype_inter s t).symm

source

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

function.bijective f → α ≃ β

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

Equations

equiv.of_bijective f hf = (equiv.set.range f _).trans ((equiv.set_congr _).trans (equiv.set.univ β))

source

@[simp]

theorem equiv.coe_of_bijective {α : Sort u_1} {β : Type u_2} {f : α → β} (hf : function.bijective f) :

⇑(equiv.of_bijective f hf) = f

source

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

function.injective f → α ≃ ↥(set.range f)

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

Equations

equiv.of_injective f hf = equiv.of_bijective (λ (x : α), ⟨f x, _⟩) _

source

@[simp]

theorem equiv.of_injective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (x : α) :

⇑(equiv.of_injective f hf) x = ⟨f x, _⟩

source

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₂

Equations

equiv.subtype_quotient_equiv_quotient_subtype p₁ p₂ hp₂ h = {to_fun := λ (a : {x // p₂ x}), a.val.hrec_on (λ (a : α) (h : (λ (x : quotient s₁), p₂ x) ⟦a⟧), ⟦⟨a, _⟩⟧) _ _, inv_fun := λ (a : quotient s₂), a.lift_on (λ (a : subtype p₁), ⟨⟦a.val ⟧, _⟩) _, left_inv := _, right_inv := _}

source

def equiv.swap_core {α : Sort u} [decidable_eq α] :

α → α → α → α

A helper function for equiv.swap.

Equations

equiv.swap_core a b r = ite (r = a) b (ite (r = b) a r)

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 α] :

α → α → equiv.perm α

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

Equations

equiv.swap a b = {to_fun := equiv.swap_core a b, inv_fun := equiv.swap_core a b, left_inv := _, right_inv := _}

source

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

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

@[simp]

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

(equiv.swap x y)⁻¹ = equiv.swap x y

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.swap_mul_self {α : Type u_1} [decidable_eq α] (i j : α) :

equiv.swap i j * equiv.swap i j = 1

source

@[simp]

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

⇑(equiv.swap i j) (⇑(equiv.swap i j) a) = a

source

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

α ≃ β → α → β → α ≃ β

Augment an equivalence with a prescribed mapping f a = b

Equations

f.set_value a b = equiv.trans (equiv.swap a (⇑(f.symm) b)) f

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 equiv.forall_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (f : α ≃ β) :

(∀ {x : α}, p x ↔ q (⇑f x)) → ((∀ (x : α), p x) ↔ ∀ (y : β), q y)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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

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

source

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

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

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

equiv.Pi_congr_left' P e = {to_fun := λ (f : Π (a : α), P a) (x : β), f (⇑(e.symm) x), inv_fun := λ (f : Π (b : β), P (⇑(e.symm) b)) (x : α), _.mpr (f (⇑e x)), left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.Pi_congr_left'_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) (f : Π (a : α), P a) (b : β) :

⇑(equiv.Pi_congr_left' P e) f b = f (⇑(e.symm) b)

source

@[simp]

theorem equiv.Pi_congr_left'_symm_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) (g : Π (b : β), P (⇑(e.symm) b)) (a : α) :

⇑((equiv.Pi_congr_left' P e).symm) g a = _.mpr (g (⇑e a))

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

equiv.Pi_congr_left P e = (equiv.Pi_congr_left' P e.symm).symm

source

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

h₁.Pi_congr h₂ = (equiv.Pi_congr_right h₂).trans (equiv.Pi_congr_left Z h₁)

source

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

h₁.Pi_congr' h₂ = (h₁.symm.Pi_congr (λ (b : β), (h₂ b).symm)).symm

source

@[instance]

def ulift.subsingleton {α : Type u_1} [subsingleton α] :

subsingleton (ulift α)

Equations

ulift.subsingleton = _

source

@[instance]

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

subsingleton (plift α)

Equations

plift.subsingleton = _

source

@[instance]

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

decidable_eq (ulift α)

Equations

ulift.decidable_eq = equiv.ulift.decidable_eq

source

@[instance]

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

decidable_eq (plift α)

Equations

plift.decidable_eq = equiv.plift.decidable_eq

source

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

α ≃ β

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

Equations

equiv_of_unique_of_unique = {to_fun := λ (_x : α), inhabited.default β, inv_fun := λ (_x : β), inhabited.default α, left_inv := _, right_inv := _}

source

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

α ≃ punit

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

Equations

equiv_punit_of_unique = equiv_of_unique_of_unique

source

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

α × α ≃ α

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

Equations

subsingleton_prod_self_equiv = {to_fun := λ (p : α × α), p.fst, inv_fun := λ (a : α), (a, a), left_inv := _, right_inv := _}

source

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

equiv_of_subsingleton_of_subsingleton f g = {to_fun := f, inv_fun := g, left_inv := _, right_inv := _}

source

def unique_unique_equiv {α : Sort u} :

unique (unique α) ≃ unique α

unique (unique α) is equivalent to unique α.

Equations

unique_unique_equiv = equiv_of_subsingleton_of_subsingleton (λ (h : unique (unique α)), inhabited.default (unique α)) (λ (h : unique α), {to_inhabited := {default := h}, uniq := _})

source

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

quot.congr e eq = {to_fun := quot.map ⇑e _, inv_fun := quot.map ⇑(e.symm) _, left_inv := _, right_inv := _}

source

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

quot.congr_right eq = quot.congr (equiv.refl α) eq

source

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

quot r ≃ quot (λ (b b' : β), r (⇑(e.symm) b) (⇑(e.symm) b'))

An equivalence e : α ≃ β generates an equivalence between the quotient space of α by a relation ra and the quotient space of β by the image of this relation under e.

Equations

quot.congr_left e = quot.congr e _

source

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

quotient.congr e eq = quot.congr e eq

source

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

quotient.congr_right eq = quot.congr_right eq

source

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

set.bij_on f set.univ s → α ≃ ↥s

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

set.bij_on.equiv f h = equiv.of_bijective (λ (x : α), ⟨f x, _⟩) _

source

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.

mathlib documentation

data.equiv.basic

General documentation

Additional documentation

Library

mathlib documentation

data.​equiv.​basic

General documentation

Additional documentation

Library

data.equiv.basic