data.equiv.basic - mathlib docs

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

equiv.perm α' ≃ equiv.perm β'

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

Equations

e.perm_congr = e.equiv_congr e

source

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

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

source

@[simp]

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

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

source

@[simp]

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

e.perm_congr.symm = e.symm.perm_congr

source

@[simp]

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

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

source

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

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

source

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

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

source

@[protected]

theorem equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :

⇑e '' s = ⇑(e.symm) ⁻¹' s

source

@[protected]

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

t ⊆ ⇑e '' s ↔ ⇑(e.symm) '' t ⊆ s

source

@[simp]

theorem equiv.symm_image_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :

⇑(e.symm) '' (⇑e '' s) = s

source

theorem equiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (t : set β) :

t = ⇑e '' s ↔ ⇑(e.symm) '' t = s

source

@[simp]

theorem equiv.image_symm_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) :

⇑e '' (⇑(e.symm) '' s) = s

source

@[simp]

theorem equiv.image_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) :

⇑e '' (⇑e ⁻¹' s) = s

source

@[simp]

theorem equiv.preimage_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :

⇑e ⁻¹' (⇑e '' s) = s

source

@[protected]

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

⇑f '' sᶜ = (⇑f '' s)ᶜ

source

@[simp]

theorem equiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) :

⇑(e.symm) ⁻¹' (⇑e ⁻¹' s) = s

source

@[simp]

theorem equiv.preimage_symm_preimage {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :

⇑e ⁻¹' (⇑(e.symm) ⁻¹' s) = s

source

@[simp]

theorem equiv.preimage_subset {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s t : set β) :

⇑e ⁻¹' s ⊆ ⇑e ⁻¹' t ↔ s ⊆ t

source

@[simp]

theorem equiv.image_subset {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s t : set α) :

⇑e '' s ⊆ ⇑e '' t ↔ s ⊆ t

source

@[simp]

theorem equiv.image_eq_iff_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s t : set α) :

⇑e '' s = ⇑e '' t ↔ s = t

source

theorem equiv.preimage_eq_iff_eq_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set β) (t : set α) :

⇑e ⁻¹' s = t ↔ s = ⇑e '' t

source

theorem equiv.eq_preimage_iff_image_eq {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (t : set β) :

s = ⇑e ⁻¹' t ↔ ⇑e '' s = t

source

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

α ≃ empty

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

Equations

equiv.equiv_empty h = {to_fun := λ (x : α), _.elim, inv_fun := λ (e : empty), empty.rec (λ (e : empty), α) e, left_inv := _, right_inv := _}

source

def equiv.false_equiv_empty :

false ≃ empty

false is equivalent to empty.

Equations

equiv.false_equiv_empty = equiv.equiv_empty id

source

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

α ≃ pempty

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

Equations

equiv.equiv_pempty h = {to_fun := λ (x : α), _.elim, inv_fun := λ (e : pempty), pempty.rec (λ (e : pempty), α) e, left_inv := _, right_inv := _}

source

def equiv.false_equiv_pempty :

false ≃ pempty

false is equivalent to pempty.

Equations

equiv.false_equiv_pempty = equiv.equiv_pempty id

source

def equiv.empty_equiv_pempty :

empty ≃ pempty

empty is equivalent to pempty.

Equations

equiv.empty_equiv_pempty = equiv.equiv_pempty equiv.empty_equiv_pempty._proof_1

source

def equiv.pempty_equiv_pempty :

pempty ≃ pempty

pempty types from any two universes are equivalent.

Equations

equiv.pempty_equiv_pempty = equiv.equiv_pempty pempty.elim

source

def equiv.empty_of_not_nonempty {α : Sort u_1} (h : ¬nonempty α) :

α ≃ empty

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

Equations

equiv.empty_of_not_nonempty h = equiv.equiv_empty _

source

def equiv.pempty_of_not_nonempty {α : Sort u_1} (h : ¬nonempty α) :

α ≃ pempty

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

Equations

equiv.pempty_of_not_nonempty h = equiv.equiv_pempty _

source

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

p ≃ punit

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

Equations

equiv.prop_equiv_punit h = {to_fun := λ (x : p), (), inv_fun := _, left_inv := _, right_inv := _}

source

def equiv.true_equiv_punit :

true ≃ punit

true is equivalent to punit.

Equations

equiv.true_equiv_punit = equiv.prop_equiv_punit trivial

source

@[simp]

theorem equiv.ulift_symm_apply {α : Type v} :

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

source

@[protected]

def equiv.ulift {α : Type v} :

ulift α ≃ α

ulift α is equivalent to α.

Equations

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

source

@[simp]

theorem equiv.ulift_apply {α : Type v} :

⇑equiv.ulift = ulift.down

source

@[simp]

theorem equiv.plift_apply {α : Sort u} :

⇑equiv.plift = plift.down

source

@[protected]

def equiv.plift {α : Sort u} :

plift α ≃ α

plift α is equivalent to α.

Equations

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

source

@[simp]

theorem equiv.plift_symm_apply {α : Sort u} :

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

source

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

P ≃ Q

equivalence of propositions is the same as iff

Equations

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

source

@[simp]

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

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

source

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

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

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

Equations

e₁.arrow_congr e₂ = {to_fun := λ (f : α₁ → β₁), ⇑e₂ ∘ f ∘ ⇑(e₁.symm), inv_fun := λ (f : α₂ → β₂), ⇑(e₂.symm) ∘ f ∘ ⇑e₁, left_inv := _, right_inv := _}

source

theorem equiv.arrow_congr_comp {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :

⇑(ea.arrow_congr ec) (g ∘ f) = ⇑(eb.arrow_congr ec) g ∘ ⇑(ea.arrow_congr eb) f

source

@[simp]

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

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

source

@[simp]

theorem equiv.arrow_congr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :

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

source

@[simp]

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

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

source

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

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

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

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

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

(α → α) ≃ (β → β)

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

Equations

e.conj = e.arrow_congr e

source

@[simp]

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

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

source

@[simp]

theorem equiv.conj_refl {α : Sort u} :

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

source

@[simp]

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

e.conj.symm = e.symm.conj

source

@[simp]

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

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

source

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

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

source

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

function.semiconj ⇑e f (⇑(e.conj) f)

source

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

function.semiconj₂ ⇑e f (⇑(e.arrow_congr e.conj) f)

source

@[protected, instance]

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

is_associative β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)

source

@[protected, instance]

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

is_idempotent β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)

source

@[protected, instance]

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

is_left_cancel β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)

source

@[protected, instance]

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

is_right_cancel β₁ (⇑(e.arrow_congr (e.arrow_congr e)) f)

source

def equiv.punit_equiv_punit :

punit ≃ punit

punit sorts in any two universes are equivalent.

Equations

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.true_arrow_equiv (α : Sort u_1) :

(true → α) ≃ α

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

Equations

equiv.true_arrow_equiv α = {to_fun := λ (f : true → α), f trivial, inv_fun := λ (a : α) (u : true), 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} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :

α₁ × β₁ ≃ α₂ × β₂

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.prod_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (x : α₁ × β₁) :

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

source

@[simp]

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

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

source

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

α × β ≃ β × α

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

Equations

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

source

@[simp]

theorem equiv.prod_comm_apply (α : Type u_1) (β : Type u_2) (ᾰ : α × β) :

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

source

@[simp]

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

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

source

@[simp]

theorem equiv.prod_assoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) :

⇑((equiv.prod_assoc α β γ).symm) p = ((p.fst, p.snd.fst), p.snd.snd)

source

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

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

Type product is associative up to an equivalence.

Equations

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

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

source

@[simp]

theorem equiv.curry_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :

⇑((equiv.curry α β γ).symm) = function.uncurry

source

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

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

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

Equations

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

source

@[simp]

theorem equiv.curry_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :

⇑(equiv.curry α β γ) = function.curry

source

def equiv.prod_punit (α : Type u_1) :

α × punit ≃ α

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

Equations

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) (p : α × punit) :

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

source

@[simp]

theorem equiv.prod_punit_symm_apply (α : Type u_1) (a : α) :

⇑((equiv.prod_punit α).symm) a = (a, punit.star)

source

def equiv.punit_prod (α : Type u_1) :

punit × α ≃ α

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

Equations

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

source

@[simp]

theorem equiv.punit_prod_symm_apply (α : Type u_1) (ᾰ : α) :

⇑((equiv.punit_prod α).symm) ᾰ = (punit.star, ᾰ)

source

@[simp]

theorem equiv.punit_prod_apply (α : Type u_1) (ᾰ : punit × α) :

⇑(equiv.punit_prod α) ᾰ = ᾰ.snd

source

def equiv.prod_empty (α : Type u_1) :

α × empty ≃ empty

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

Equations

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

@[simp]

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

⇑(ea.sum_congr eb) ᾰ = sum.map ⇑ea ⇑eb ᾰ

source

def equiv.sum_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) :

α₁ ⊕ β₁ ≃ α₂ ⊕ β₂

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

Equations

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_trans {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) :

(e.sum_congr f).trans (g.sum_congr h) = (e.trans g).sum_congr (f.trans h)

source

@[simp]

theorem equiv.sum_congr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (f : γ ≃ δ) :

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

source

@[simp]

theorem equiv.sum_congr_refl {α : Type u_1} {β : Type u_2} :

(equiv.refl α).sum_congr (equiv.refl β) = equiv.refl (α ⊕ β)

source

def equiv.perm.sum_congr {α : Type u_1} {β : Type u_2} (ea : equiv.perm α) (eb : equiv.perm β) :

equiv.perm (α ⊕ β)

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

Equations

ea.sum_congr eb = equiv.sum_congr ea eb

source

@[simp]

theorem equiv.perm.sum_congr_apply {α : Type u_1} {β : Type u_2} (ea : equiv.perm α) (eb : equiv.perm β) (x : α ⊕ β) :

⇑(ea.sum_congr eb) x = sum.map ⇑ea ⇑eb x

source

@[simp]

theorem equiv.perm.sum_congr_trans {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) (g : equiv.perm α) (h : equiv.perm β) :

equiv.trans (e.sum_congr f) (g.sum_congr h) = equiv.perm.sum_congr (equiv.trans e g) (equiv.trans f h)

source

@[simp]

theorem equiv.perm.sum_congr_symm {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) :

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

source

@[simp]

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

equiv.perm.sum_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α ⊕ β)

source

def equiv.bool_equiv_punit_sum_punit :

bool ≃ punit ⊕ punit

bool is equivalent the sum of two punits.

Equations

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), ff) (λ (_x : punit), 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), 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

@[simp]

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

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

source

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

α ⊕ β ≃ β ⊕ α

Sum of types is commutative up to an equivalence.

Equations

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

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_symm_apply (α : Type u_1) (val : α) :

⇑((equiv.sum_empty α).symm) val = sum.inl val

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_symm_apply (α : Type u_1) (ᾰ : α) :

⇑((equiv.empty_sum α).symm) ᾰ = sum.inr ᾰ

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_symm_apply (α : Type u_1) (val : α) :

⇑((equiv.sum_pempty α).symm) val = sum.inl val

source

@[simp]

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

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

source

@[simp]

theorem equiv.pempty_sum_symm_apply (α : Type u_1) (ᾰ : α) :

⇑((equiv.pempty_sum α).symm) ᾰ = sum.inr ᾰ

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 α (some a) = sum.inl a
equiv.option_equiv_sum_punit._match_1 α none = sum.inr punit.star
equiv.option_equiv_sum_punit._match_2 α (sum.inr _x) = none
equiv.option_equiv_sum_punit._match_2 α (sum.inl a) = some a

source

@[simp]

theorem equiv.option_equiv_sum_punit_none {α : Type u_1} :

⇑(equiv.option_equiv_sum_punit α) none = sum.inr punit.star

source

@[simp]

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

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

source

@[simp]

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

⇑(equiv.option_equiv_sum_punit α) ↑a = sum.inl a

source

@[simp]

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

⇑((equiv.option_equiv_sum_punit α).symm) (sum.inl a) = ↑a

source

@[simp]

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

⇑((equiv.option_equiv_sum_punit α).symm) (sum.inr a) = none

source

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 : α), ⟨some x, _⟩, left_inv := _, right_inv := _}

source

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

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

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

Equations

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

source

@[simp]

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

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

source

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

(Σ (y : β), {x // f x = y}) ≃ α

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

Equations

equiv.sigma_preimage_equiv f = {to_fun := λ (x : Σ (y : β), {x // f x = y}), ↑(x.snd), 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)

source

@[simp]

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

↑((⇑((equiv.sigma_preimage_equiv f).symm) x).snd) = x

source

def equiv.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

equiv.set_prod_equiv_sigma s = {to_fun := λ (x : ↥s), ⟨x.val.fst, ⟨x.val.snd, _⟩⟩, inv_fun := λ (x : Σ (x : α), ↥{y : β | (x, y) ∈ s}), ⟨(x.fst, x.snd.val), _⟩, left_inv := _, right_inv := _}

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_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) (f : {x // ¬p x} ≃ {x // ¬q x}) :

equiv.perm α

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

Equations

e.subtype_congr f = (equiv.sum_compl p).symm.trans ((e.sum_congr f).trans (equiv.sum_compl q))

source

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

equiv.perm ε

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

Equations

ep.subtype_congr en = ⇑((equiv.sum_compl p).perm_congr) (equiv.sum_congr ep en)

source

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

⇑(ep.subtype_congr en) a = dite (p a) (λ (h : p a), ↑(⇑ep ⟨a, h⟩)) (λ (h : ¬p a), ↑(⇑en ⟨a, h⟩))

source

@[simp]

theorem equiv.perm.subtype_congr.left_apply {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : p a) :

⇑(ep.subtype_congr en) a = ↑(⇑ep ⟨a, h⟩)

source

@[simp]

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

⇑(ep.subtype_congr en) ↑a = ↑(⇑ep a)

source

@[simp]

theorem equiv.perm.subtype_congr.right_apply {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : ¬p a) :

⇑(ep.subtype_congr en) a = ↑(⇑en ⟨a, h⟩)

source

@[simp]

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

⇑(ep.subtype_congr en) ↑a = ↑(⇑en a)

source

@[simp]

theorem equiv.perm.subtype_congr.refl {ε : Type u_1} {p : ε → Prop} [decidable_pred p] :

equiv.perm.subtype_congr (equiv.refl {a // p a}) (equiv.refl {a // ¬p a}) = equiv.refl ε

source

@[simp]

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

equiv.symm (ep.subtype_congr en) = equiv.perm.subtype_congr (equiv.symm ep) (equiv.symm en)

source

@[simp]

theorem equiv.perm.subtype_congr.trans {ε : Type u_1} {p : ε → Prop} [decidable_pred p] (ep ep' : equiv.perm {a // p a}) (en en' : equiv.perm {a // ¬p a}) :

equiv.trans (ep.subtype_congr en) (ep'.subtype_congr en') = equiv.perm.subtype_congr (equiv.trans ep ep') (equiv.trans en en')

source

@[simp]

theorem equiv.subtype_preimage_symm_apply_coe {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) :

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

source

@[simp]

theorem equiv.subtype_preimage_apply {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) (x : {x // x ∘ coe = x₀}) (a : {a // ¬p a}) :

⇑(equiv.subtype_preimage p x₀) x a = ↑x ↑a

source

def equiv.subtype_preimage {α : Sort u} {β : Sort v} (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) :

{x // x ∘ coe = x₀} ≃ ({a // ¬p a} → β)

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

Equations

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

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 (default α), inv_fun := λ (b : β) (a : α), b, left_inv := _, right_inv := _}

source

@[simp]

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

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

source

@[simp]

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

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

source

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

(Π (a : α), β₁ a) ≃ Π (a : α), β₂ a

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

Equations

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 → Type u_3) :

(Π (x : Σ (i : α), β i), γ x.fst x.snd) ≃ Π (a : α) (b : β a), γ a b

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

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

Equations

equiv.Pi_curry γ = {to_fun := sigma.curry γ, inv_fun := sigma.uncurry (λ (a : α) (b : β a), γ a b), 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_symm_apply {α : Type u_1} (β : α → Type u_2) (a : Σ (i : α), β i) :

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

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

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

equiv.perm (Σ (a : α), β a)

A family of permutations Π a, perm (β a) generates a permuation perm (Σ a, β₁ a).

Equations

equiv.perm.sigma_congr_right F = equiv.sigma_congr_right F

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

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

Equations

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

source

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

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

Transporting a sigma type through an equivalence of the base

Equations

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

source

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

sigma β₁ ≃ sigma β₂

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

Equations

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

source

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

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

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

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

sigma β₁ ≃ α × β

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

Equations

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

source

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

β₁ × α₁ ≃ β₂ × α₁

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

Equations

equiv.prod_congr_left e = {to_fun := λ (ab : β₁ × α₁), (⇑(e ab.snd) ab.fst, ab.snd), inv_fun := λ (ab : β₂ × α₁), (⇑((e ab.snd).symm) ab.fst, ab.snd), left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.prod_congr_left_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) (b : β₁) (a : α₁) :

⇑(equiv.prod_congr_left e) (b, a) = (⇑(e a) b, a)

source

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

e.prod_congr (equiv.refl α₁) = equiv.prod_congr_left (λ (_x : α₁), e)

source

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

α₁ × β₁ ≃ α₁ × β₂

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

Equations

equiv.prod_congr_right e = {to_fun := λ (ab : α₁ × β₁), (ab.fst, ⇑(e ab.fst) ab.snd), inv_fun := λ (ab : α₁ × β₂), (ab.fst, ⇑((e ab.fst).symm) ab.snd), left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.prod_congr_right_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ ≃ β₂) (a : α₁) (b : β₁) :

⇑(equiv.prod_congr_right e) (a, b) = (a, ⇑(e a) b)

source

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

(equiv.refl α₁).prod_congr e = equiv.prod_congr_right (λ (_x : α₁), e)

source

@[simp]

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

(equiv.prod_congr_left e).trans (equiv.prod_comm β₂ α₁) = (equiv.prod_comm β₁ α₁).trans (equiv.prod_congr_right e)

source

@[simp]

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

(equiv.prod_congr_right e).trans (equiv.prod_comm α₁ β₂) = (equiv.prod_comm α₁ β₁).trans (equiv.prod_congr_left e)

source

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

(equiv.sigma_congr_right e).trans (equiv.sigma_equiv_prod α₁ β₂) = (equiv.sigma_equiv_prod α₁ β₁).trans (equiv.prod_congr_right e)

source

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

(equiv.sigma_equiv_prod α₁ β₁).symm.trans (equiv.sigma_congr_right e) = (equiv.prod_congr_right e).trans (equiv.sigma_equiv_prod α₁ β₂).symm

source

@[simp]

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

⇑((e₁.prod_shear e₂).symm) = λ (y : α₂ × β₂), (⇑(e₁.symm) y.fst, ⇑((e₂ (⇑(e₁.symm) y.fst)).symm) y.snd)

source

@[simp]

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

⇑(e₁.prod_shear e₂) = λ (x : α₁ × β₁), (⇑e₁ x.fst, ⇑(e₂ x.fst) x.snd)

source

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

α₁ × β₁ ≃ α₂ × β₂

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

Equations

e₁.prod_shear e₂ = {to_fun := λ (x : α₁ × β₁), (⇑e₁ x.fst, ⇑(e₂ x.fst) x.snd), inv_fun := λ (y : α₂ × β₂), (⇑(e₁.symm) y.fst, ⇑((e₂ (⇑(e₁.symm) y.fst)).symm) y.snd), left_inv := _, right_inv := _}

source

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

equiv.perm (α₁ × β₁)

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

Equations

equiv.perm.prod_extend_right a e = {to_fun := λ (ab : α₁ × β₁), ite (ab.fst = a) (a, ⇑e ab.snd) ab, inv_fun := λ (ab : α₁ × β₁), ite (ab.fst = a) (a, ⇑(equiv.symm e) ab.snd) ab, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.perm.prod_extend_right_apply_eq {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (b : β₁) :

⇑(equiv.perm.prod_extend_right a e) (a, b) = (a, ⇑e b)

source

theorem equiv.perm.prod_extend_right_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (e : equiv.perm β₁) {a a' : α₁} (h : a' ≠ a) (b : β₁) :

⇑(equiv.perm.prod_extend_right a e) (a', b) = (a', b)

source

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

a' = a

source

@[simp]

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

(⇑(equiv.perm.prod_extend_right a e) ab).fst = ab.fst

source

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

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

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

Equations

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.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.bool_to_equiv_prod (α : Type u) :

(bool → α) ≃ α × α

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

Equations

equiv.bool_to_equiv_prod α = ((equiv.bool_equiv_punit_sum_punit.arrow_congr (equiv.refl α)).trans (equiv.sum_arrow_equiv_prod_arrow unit unit α)).trans ((equiv.punit_arrow_equiv α).prod_congr (equiv.punit_arrow_equiv α))

source

@[simp]

theorem equiv.bool_to_equiv_prod_apply {α : Type u} (f : bool → α) :

⇑(equiv.bool_to_equiv_prod α) f = (f ff, f tt)

source

@[simp]

theorem equiv.bool_to_equiv_prod_symm_apply_ff {α : Type u} (p : α × α) :

⇑((equiv.bool_to_equiv_prod α).symm) p ff = p.fst

source

@[simp]

theorem equiv.bool_to_equiv_prod_symm_apply_tt {α : Type u} (p : α × α) :

⇑((equiv.bool_to_equiv_prod α).symm) p tt = p.snd

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} (e : α ≃ β) :

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} (e : α ≃ β) :

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_equiv {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (⇑e a)) :

{a // p a} ≃ {b // q b}

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

Equations

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

source

@[simp]

theorem equiv.subtype_equiv_refl {α : Sort u} {p : α → Prop} (h : (∀ (a : α), p a ↔ p (⇑(equiv.refl α) a)) := _) :

(equiv.refl α).subtype_equiv h = equiv.refl {a // p a}

source

@[simp]

theorem equiv.subtype_equiv_symm {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (⇑e a)) :

(e.subtype_equiv h).symm = e.symm.subtype_equiv _

source

@[simp]

theorem equiv.subtype_equiv_trans {α : Sort u} {β : Sort v} {γ : Sort w} {p : α → Prop} {q : β → Prop} {r : γ → Prop} (e : α ≃ β) (f : β ≃ γ) (h : ∀ (a : α), p a ↔ q (⇑e a)) (h' : ∀ (b : β), q b ↔ r (⇑f b)) :

(e.subtype_equiv h).trans (f.subtype_equiv h') = (e.trans f).subtype_equiv _

source

@[simp]

theorem equiv.subtype_equiv_apply {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (⇑e a)) (x : {x // p x}) :

⇑(e.subtype_equiv h) x = ⟨⇑e ↑x, _⟩

source

@[simp]

theorem equiv.subtype_equiv_right_symm_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (y : {b // (λ (x : α), q x) b}) :

↑(⇑((equiv.subtype_equiv_right e).symm) y) = ↑y

source

def equiv.subtype_equiv_right {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) :

{x // p x} ≃ {x // q x}

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

Equations

equiv.subtype_equiv_right e = (equiv.refl α).subtype_equiv e

source

@[simp]

theorem equiv.subtype_equiv_right_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (x : {a // (λ (x : α), p x) a}) :

↑(⇑(equiv.subtype_equiv_right e) x) = ↑x

source

def equiv.subtype_equiv_of_subtype {α : Sort u} {β : Sort v} {p : β → Prop} (e : α ≃ β) :

{a // p (⇑e a)} ≃ {b // p b}

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

Equations

e.subtype_equiv_of_subtype = e.subtype_equiv _

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_equiv_prop {α : Type u_1} {p q : α → Prop} (h : p = q) :

subtype p ≃ subtype q

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

Equations

equiv.subtype_equiv_prop h = (equiv.refl α).subtype_equiv _

source

def equiv.set_congr {α : Type u_1} {s t : set α} (h : s = t) :

↥s ≃ ↥t

The subtypes corresponding to equal sets are equivalent.

Equations

equiv.set_congr h = equiv.subtype_equiv_prop h

source

@[simp]

theorem equiv.set_congr_apply {α : Type u_1} {s t : set α} (h : s = t) (x : {a // (λ (a : α), (λ (x : α), x ∈ s) a) a}) :

⇑(equiv.set_congr h) x = ⟨↑x, _⟩

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

@[simp]

theorem equiv.subtype_subtype_equiv_subtype_exists_apply {α : Type u} (p : α → Prop) (q : subtype p → Prop) (a : subtype q) :

↑(⇑(equiv.subtype_subtype_equiv_subtype_exists p q) a) = ↑a

source

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

{x // q x.val} ≃ {x // p x ∧ q x}

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

Equations

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

source

@[simp]

theorem equiv.subtype_subtype_equiv_subtype_inter_apply {α : Type u} (p q : α → Prop) (a : {x // q x.val}) :

↑(⇑(equiv.subtype_subtype_equiv_subtype_inter p q) a) = ↑a

source

def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) :

{x // q x.val} ≃ subtype q

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

Equations

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

source

@[simp]

theorem equiv.subtype_subtype_equiv_subtype_apply {α : Type u} {p q : α → Prop} (h : ∀ (x : α), q x → p x) (a : {x // q x.val}) :

↑(⇑(equiv.subtype_subtype_equiv_subtype h) a) = ↑a

source

def equiv.subtype_univ_equiv {α : Type u} {p : α → Prop} (h : ∀ (x : α), p x) :

subtype p ≃ α

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

Equations

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

source

@[simp]

theorem equiv.subtype_univ_equiv_symm_apply {α : Type u} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) :

⇑((equiv.subtype_univ_equiv h).symm) x = ⟨x, _⟩

source

@[simp]

theorem equiv.subtype_univ_equiv_apply {α : Type u} {p : α → Prop} (h : ∀ (x : α), p x) (x : subtype p) :

⇑(equiv.subtype_univ_equiv h) x = ↑x

source

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

{y // q y.fst} ≃ Σ (x : subtype q), p x.val

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

Equations

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

(Σ (x : subtype q), p ↑x) ≃ Σ (x : α), p x

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

Equations

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) (h : ∀ (x : α), p (f x)) :

(Σ (y : subtype p), {x // f x = ↑y}) ≃ α

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

Equations

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} (h : ∀ (x : α), p x ↔ q (f x)) :

(Σ (y : subtype q), {x // f x = ↑y}) ≃ subtype p

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

Equations

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

@[simp]

theorem equiv.image_apply_coe {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (x : ↥s) :

↑(⇑(e.image s) x) = ⇑e x.val

source

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

↥s ≃ ↥(⇑e '' s)

A set is equivalent to its image under an equivalence.

Equations

e.image s = {to_fun := λ (x : ↥s), ⟨⇑e x.val, _⟩, inv_fun := λ (y : ↥(⇑e '' s)), ⟨⇑(e.symm) y.val, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.image_symm_apply_coe {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) (y : ↥(⇑e '' s)) :

↑(⇑((e.image s).symm) y) = ⇑(e.symm) y.val

source

@[simp]

theorem equiv.set.univ_symm_apply (α : Type u_1) (a : α) :

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

source

@[protected]

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

↥set.univ ≃ α

univ α is equivalent to α.

Equations

equiv.set.univ α = {to_fun := coe coe_to_lift, inv_fun := λ (a : α), ⟨a, trivial⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.set.univ_apply (α : Type u_1) (ᾰ : ↥set.univ) :

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

source

@[protected]

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

@[protected]

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

@[protected]

def equiv.set.union' {α : Type u_1} {s t : set α} (p : α → Prop) [decidable_pred p] (hs : ∀ (x : α), x ∈ s → p x) (ht : ∀ (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

@[protected]

def equiv.set.union {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : 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

@[simp]

theorem equiv.set.union_symm_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) (a : ↥s) :

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

source

@[simp]

theorem equiv.set.union_symm_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x ∈ s)] (H : s ∩ t ⊆ ∅) (a : ↥t) :

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

source

@[protected]

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

@[simp]

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

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

source

@[protected]

def equiv.set.of_eq {α : Type u} {s t : set α} (h : s = t) :

↥s ≃ ↥t

Equal sets are equivalent.

Equations

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

source

@[simp]

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

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

source

@[protected]

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

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

@[simp]

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

⇑((equiv.set.insert H).symm) (sum.inl b) = ⟨↑b, _⟩

source

@[simp]

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

⇑((equiv.set.insert H).symm) (sum.inr b) = ⟨a, _⟩

source

@[simp]

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

⇑(equiv.set.insert H) ⟨a, _⟩ = sum.inr punit.star

source

@[simp]

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

⇑(equiv.set.insert H) ⟨↑b, _⟩ = sum.inl b

source

@[protected]

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

@[simp]

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

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

source

@[simp]

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

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

source

@[protected]

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

@[protected]

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

@[protected]

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

equiv.set.compl e₀ = {to_fun := λ (e : {e // ∀ (x : ↥s), ⇑e ↑x = ↑(⇑e₀ x)}), ↑e.subtype_equiv _, inv_fun := λ (e₁ : ↥sᶜ ≃ ↥tᶜ), ⟨((equiv.set.sum_compl s).symm.trans (e₀.sum_congr e₁)).trans (equiv.set.sum_compl t (λ (a : β), _inst_2 a)), _⟩, left_inv := _, right_inv := _}

source

@[protected]

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

@[protected]

def equiv.set.image_of_inj_on {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : 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

@[protected]

def equiv.set.image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : 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) (p : ↥s) :

⇑(equiv.set.image f s H) p = ⟨f ↑p, _⟩

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

@[simp]

theorem equiv.set.congr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : set α) :

⇑(equiv.set.congr e) s = ⇑e '' s

source

@[protected]

def equiv.set.congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

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

@[simp]

theorem equiv.set.congr_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (t : set β) :

⇑((equiv.set.congr e).symm) t = ⇑(e.symm) '' t

source

@[protected]

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

@[protected]

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

↥𝒫S ≃ set ↥S

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

Equations

equiv.set.powerset S = {to_fun := λ (x : ↥𝒫S), coe ⁻¹' ↑x, inv_fun := λ (x : set ↥S), ⟨coe '' x, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.of_left_inverse_symm_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) (b : ↥(set.range f)) :

⇑((equiv.of_left_inverse f f_inv hf).symm) b = f_inv _ ↑b

source

def equiv.of_left_inverse {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) :

α ≃ ↥(set.range f)

If f : α → β has a left-inverse when α is nonempty, then α is computably equivalent to the range of f.

While awkward, the nonempty α hypothesis on f_inv and hf allows this to be used when α is empty too. This hypothesis is absent on analogous definitions on stronger equivs like linear_equiv.of_left_inverse and ring_equiv.of_left_inverse as their typeclass assumptions are already sufficient to ensure non-emptiness.

Equations

equiv.of_left_inverse f f_inv hf = {to_fun := λ (a : α), ⟨f a, _⟩, inv_fun := λ (b : ↥(set.range f)), f_inv _ ↑b, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.of_left_inverse_apply_coe {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) (a : α) :

↑(⇑(equiv.of_left_inverse f f_inv hf) a) = f a

source

def equiv.of_left_inverse' {α : Sort u_1} {β : Type u_2} (f : α → β) (f_inv : β → α) (hf : function.left_inverse f_inv f) :

α ≃ ↥(set.range f)

If f : α → β has a left-inverse, then α is computably equivalent to the range of f.

Note that if α is empty, no such f_inv exists and so this definition can't be used, unlike the stronger but less convenient of_left_inverse.

source

@[simp]

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

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

source

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

α ≃ ↥(set.range f)

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

Equations

equiv.of_injective f hf = equiv.of_left_inverse f (λ (h : nonempty α), function.inv_fun f) _

source

theorem equiv.apply_of_injective_symm {α : Type u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (b : ↥(set.range f)) :

f (⇑((equiv.of_injective f hf).symm) b) = ↑b

source

@[simp]

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

f ∘ ⇑((equiv.of_injective f hf).symm) = coe

source

theorem equiv.of_left_inverse_eq_of_injective {α : Type u_1} {β : Type u_2} (f : α → β) (f_inv : nonempty α → β → α) (hf : ∀ (h : nonempty α), function.left_inverse (f_inv h) f) :

equiv.of_left_inverse f f_inv hf = equiv.of_injective f _

source

theorem equiv.of_left_inverse'_eq_of_injective {α : Type u_1} {β : Type u_2} (f : α → β) (f_inv : β → α) (hf : function.left_inverse f_inv f) :

equiv.of_left_inverse' f f_inv hf = equiv.of_injective f _

source

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

α ≃ β

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

Equations

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

source

@[simp]

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

⇑(equiv.of_bijective f hf) ᾰ = f ᾰ

source

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

f (⇑((equiv.of_bijective f hf).symm) x) = x

source

@[simp]

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

⇑((equiv.of_bijective f hf).symm) (f x) = x

source

def equiv.perm.extend_domain {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) :

equiv.perm β'

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

Equations

e.extend_domain f = (⇑(f.perm_congr) e).subtype_congr (equiv.refl {a // ¬p a})

source

@[simp]

theorem equiv.perm.extend_domain_apply_image {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) (a : α') :

⇑(e.extend_domain f) ↑(⇑f a) = ↑(⇑f (⇑e a))

source

theorem equiv.perm.extend_domain_apply_subtype {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) {b : β'} (h : p b) :

⇑(e.extend_domain f) b = ↑(⇑f (⇑e (⇑(f.symm) ⟨b, h⟩)))

source

theorem equiv.perm.extend_domain_apply_not_subtype {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) {b : β'} (h : ¬p b) :

⇑(e.extend_domain f) b = b

source

@[simp]

theorem equiv.perm.extend_domain_refl {α' : Type u_1} {β' : Type u_2} {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) :

equiv.perm.extend_domain (equiv.refl α') f = equiv.refl β'

source

@[simp]

theorem equiv.perm.extend_domain_symm {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) :

equiv.symm (e.extend_domain f) = equiv.perm.extend_domain (equiv.symm e) f

source

theorem equiv.perm.extend_domain_trans {α' : Type u_1} {β' : Type u_2} {p : β' → Prop} [decidable_pred p] (f : α' ≃ subtype p) (e e' : equiv.perm α') :

equiv.trans (e.extend_domain f) (e'.extend_domain f) = equiv.perm.extend_domain (equiv.trans e e') f

source

def equiv.subtype_quotient_equiv_quotient_subtype {α : Sort u} (p₁ : α → Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : subtype p₁), setoid.r x y ↔ ↑x ≈ ↑y) :

{x // p₂ x} ≃ quotient s₂

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

Equations

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 b r : α) :

α

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 α] (a b : α) :

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

@[simp]

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

equiv.swap a a = equiv.refl α

source

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

equiv.swap a b = equiv.swap b a

source

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

⇑(equiv.swap a b) x = ite (x = a) b (ite (x = b) a x)

source

@[simp]

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

⇑(equiv.swap a b) a = b

source

@[simp]

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

⇑(equiv.swap a b) b = a

source

theorem equiv.swap_apply_of_ne_of_ne {α : Sort u} [decidable_eq α] {a b x : α} :

x ≠ a → x ≠ b → ⇑(equiv.swap a b) x = x

source

@[simp]

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

equiv.trans (equiv.swap a b) (equiv.swap a b) = equiv.refl α

source

@[simp]

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

equiv.symm (equiv.swap a b) = equiv.swap a b

source

@[simp]

theorem equiv.swap_eq_refl_iff {α : Sort u} [decidable_eq α] {x y : α} :

equiv.swap x y = equiv.refl α ↔ x = y

source

theorem equiv.swap_comp_apply {α : Sort u} [decidable_eq α] {a b x : α} (π : equiv.perm α) :

⇑(equiv.trans «π» (equiv.swap a b)) x = ite (⇑«π» x = a) b (ite (⇑«π» x = b) a (⇑«π» x))

source

theorem equiv.swap_eq_update {α : Sort u} [decidable_eq α] (i j : α) :

⇑(equiv.swap i j) = function.update (function.update id j i) i j

source

theorem equiv.comp_swap_eq_update {α : Sort u} {β : Sort v} [decidable_eq α] (i j : α) (f : α → β) :

f ∘ ⇑(equiv.swap i j) = function.update (function.update f j (f i)) i (f j)

source

@[simp]

theorem equiv.symm_trans_swap_trans {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : α) (e : α ≃ β) :

(e.symm.trans (equiv.swap a b)).trans e = equiv.swap (⇑e a) (⇑e b)

source

@[simp]

theorem equiv.trans_swap_trans_symm {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : β) (e : α ≃ β) :

(e.trans (equiv.swap a b)).trans e.symm = equiv.swap (⇑(e.symm) a) (⇑(e.symm) b)

source

@[simp]

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

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

source

theorem equiv.apply_swap_eq_self {α : Sort u} {β : Sort v} [decidable_eq α] {v : α → β} {i j : α} (hv : v i = v j) (k : α) :

v (⇑(equiv.swap i j) k) = v k

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

source

theorem equiv.swap_apply_eq_iff {α : Sort u} [decidable_eq α] {x y z w : α} :

⇑(equiv.swap x y) z = w ↔ z = ⇑(equiv.swap x y) w

source

@[simp]

theorem equiv.perm.sum_congr_swap_refl {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : α) :

(equiv.swap i j).sum_congr (equiv.refl β) = equiv.swap (sum.inl i) (sum.inl j)

source

@[simp]

theorem equiv.perm.sum_congr_refl_swap {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (i j : β) :

equiv.perm.sum_congr (equiv.refl α) (equiv.swap i j) = equiv.swap (sum.inr i) (sum.inr j)

source

def equiv.set_value {α : Sort u} {β : Sort v} [decidable_eq α] (f : α ≃ β) (a : α) (b : β) :

α ≃ β

Augment an equivalence with a prescribed mapping f a = b

Equations

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 function.injective.map_swap {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α → β} (hf : function.injective f) (x y z : α) :

f (⇑(equiv.swap x y) z) = ⇑(equiv.swap (f x) (f y)) (f z)

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

(∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z

source

@[protected]

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

(∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

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

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

source

@[protected]

theorem equiv.set_forall_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) {p : set α → Prop} :

(∀ (a : set α), p a) ↔ ∀ (a : set β), p (⇑e ⁻¹' a)

source

@[protected]

theorem equiv.preimage_sUnion {α : Type u_1} {β : Type u_2} (f : α ≃ β) {s : set (set β)} :

⇑f ⁻¹' ⋃₀s = ⋃₀(set.image ⇑f ⁻¹' s)

source

@[simp]

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

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

source

def equiv.Pi_congr_left' {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) :

(Π (a : α), P a) ≃ Π (b : β), P (⇑(e.symm) b)

Transport dependent functions through an equivalence of the base space.

Equations

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'_symm_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α ≃ β) (f : Π (b : β), P (⇑(e.symm) b)) (x : α) :

⇑((equiv.Pi_congr_left' P e).symm) f x = _.mpr (f (⇑e x))

source

def equiv.Pi_congr_left {α : Sort u} {β : Sort v} (P : β → Sort w) (e : α ≃ β) :

(Π (a : α), P (⇑e a)) ≃ Π (b : β), P b

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

Equations

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₁ : α ≃ β) (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₁ : α ≃ β) (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

theorem function.injective.swap_apply {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] {f : α → β} (hf : function.injective f) (x y z : α) :

⇑(equiv.swap (f x) (f y)) (f z) = f (⇑(equiv.swap x y) z)

source

theorem function.injective.swap_comp {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] {f : α → β} (hf : function.injective f) (x y : α) :

⇑(equiv.swap (f x) (f y)) ∘ f = f ∘ ⇑(equiv.swap x y)

source

@[protected, instance]

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

subsingleton (ulift α)

source

@[protected, instance]

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

subsingleton (plift α)

source

@[protected, instance]

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

unique (ulift α)

Equations

ulift.unique = equiv.ulift.unique

source

@[protected, instance]

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

unique (plift α)

Equations

plift.unique = equiv.plift.unique

source

@[protected, instance]

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

decidable_eq (ulift α)

Equations

ulift.decidable_eq = equiv.ulift.decidable_eq

source

@[protected, 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 : α), default β, inv_fun := λ (_x : β), 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 β] (f : α → β) (g : β → α) :

α ≃ β

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 equiv.punit_of_nonempty_of_subsingleton {α : Sort u_1} [h : nonempty α] [subsingleton α] :

α ≃ punit

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

Equations

equiv.punit_of_nonempty_of_subsingleton = equiv_of_subsingleton_of_subsingleton (λ (_x : α), punit.star) (λ (_x : punit), h.some)

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 α)), default (unique α)) (λ (h : unique α), {to_inhabited := {default := h}, uniq := _})

source

@[protected]

def quot.congr {α : Sort u} {β : Sort v} {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (⇑e a₁) (⇑e a₂)) :

quot ra ≃ quot rb

An equivalence e : α ≃ β generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Equations

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

source

@[protected]

def quot.congr_right {α : Sort u} {r r' : α → α → Prop} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) :

quot r ≃ quot r'

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

Equations

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

source

@[protected]

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

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

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

Equations

quot.congr_left e = quot.congr e _

source

@[protected]

def quotient.congr {α : Sort u} {β : Sort v} {ra : setoid α} {rb : setoid β} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), setoid.r a₁ a₂ ↔ setoid.r (⇑e a₁) (⇑e a₂)) :

quotient ra ≃ quotient rb

An equivalence e : α ≃ β generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Equations

quotient.congr e eq = quot.congr e eq

source

@[protected]

def quotient.congr_right {α : Sort u} {r r' : setoid α} (eq : ∀ (a₁ a₂ : α), setoid.r a₁ a₂ ↔ setoid.r a₁ a₂) :

quotient r ≃ quotient r'

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with eq, but then computational proofs get stuck.

Equations

quotient.congr_right eq = quot.congr_right eq

source

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

↥s ≃ ↥t

If a function is a bijection between two sets s and t, then it induces an equivalence between the the types ↥s and ``↥t`.

Equations

set.bij_on.equiv f h = equiv.of_bijective (set.cod_restrict (set.restrict f s) t _) _

source

theorem function.update_comp_equiv {α : Sort u_1} {β : Sort u_2} {α' : Sort u_3} [decidable_eq α'] [decidable_eq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) :

function.update f a v ∘ ⇑g = function.update (f ∘ ⇑g) (⇑(g.symm) a) v

source

theorem function.update_apply_equiv_apply {α : Sort u_1} {β : Sort u_2} {α' : Sort u_3} [decidable_eq α'] [decidable_eq α] (f : α → β) (g : α' ≃ α) (a : α) (v : β) (a' : α') :

function.update f a v (⇑g a') = function.update (f ∘ ⇑g) (⇑(g.symm) a) v a'

source

theorem dite_comp_equiv_update {α : Type u_1} {β : Sort u_2} {γ : Sort 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

Equivalence between types #

Tags #