Documentation

🔶 coverage

structure Equiv (α : Sort u_1) (β : Sort u_2) :

Sort (max (max 1 u_1) u_2)

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

toFun : α → β
The forward map of an equivalence.
Do NOT use directly. Use the coercion instead.
invFun : β → α
The backward map of an equivalence.
Do NOT use e.invFun directly. Use the coercion of e.symm instead.
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun

Instances For

def «term_≃_» :

Lean.TrailingParserDescr

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

Equations

Instances For

def EquivLike.toEquiv {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (f : F) :

α ≃ β

Turn an element of a type F satisfying EquivLike F α β into an actual Equiv. This is declared as the default coercion from F to α ≃ β.

Equations

Instances For

instance instCoeTCEquivOfEquivLike {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] :

CoeTC F (α ≃ β)

Any type satisfying EquivLike can be cast into Equiv via EquivLike.toEquiv.

Equations

@[reducible, inline]

abbrev Equiv.Perm (α : Sort u_1) :

Sort (max 1 u_1)

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

Equations

Instances For

instance Equiv.instEquivLike {α : Sort u} {β : Sort v} :

EquivLike (α ≃ β) α β

Equations

@[simp]

theorem EquivLike.coe_coe {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) :

⇑↑e = ⇑e

@[simp]

theorem Equiv.coe_fn_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) :

⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f

theorem Equiv.coe_fn_injective {α : Sort u} {β : Sort v} :

Function.Injective fun (e : α ≃ β) => ⇑e

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

theorem Equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β} :

⇑e₁ = ⇑e₂ ↔ e₁ = e₂

theorem Equiv.ext {α : Sort u} {β : Sort v} {f g : α ≃ β} (H : ∀ (x : α), f x = g x) :

f = g

theorem Equiv.ext_iff {α : Sort u} {β : Sort v} {f g : α ≃ β} :

f = g ↔ ∀ (x : α), f x = g x

theorem Equiv.congr_arg {α : Sort u} {β : Sort v} {f : α ≃ β} {x x' : α} :

x = x' → f x = f x'

theorem Equiv.congr_fun {α : Sort u} {β : Sort v} {f g : α ≃ β} (h : f = g) (x : α) :

f x = g x

theorem Equiv.Perm.ext {α : Sort u} {σ τ : Perm α} (H : ∀ (x : α), σ x = τ x) :

σ = τ

theorem Equiv.Perm.ext_iff {α : Sort u} {σ τ : Perm α} :

σ = τ ↔ ∀ (x : α), σ x = τ x

theorem Equiv.Perm.congr_arg {α : Sort u} {f : Perm α} {x x' : α} :

x = x' → f x = f x'

theorem Equiv.Perm.congr_fun {α : Sort u} {f g : Perm α} (h : f = g) (x : α) :

f x = g x

def Equiv.refl (α : Sort u_1) :

α ≃ α

Any type is equivalent to itself.

Equations

Instances For

instance Equiv.inhabited' {α : Sort u} :

Inhabited (α ≃ α)

Equations

def Equiv.symm {α : Sort u} {β : Sort v} (e : α ≃ β) :

β ≃ α

Inverse of an equivalence e : α ≃ β.

Equations

Instances For

def Equiv.Simps.symm_apply {α : Sort u} {β : Sort v} (e : α ≃ β) :

β → α

See Note [custom simps projection]

Equations

Instances For

theorem Equiv.left_inv' {α : Sort u} {β : Sort v} (e : α ≃ β) :

Function.LeftInverse ⇑e.symm ⇑e

Restatement of Equiv.left_inv in terms of Function.LeftInverse.

theorem Equiv.right_inv' {α : Sort u} {β : Sort v} (e : α ≃ β) :

Function.RightInverse ⇑e.symm ⇑e

Restatement of Equiv.right_inv in terms of Function.RightInverse.

def Equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) :

α ≃ γ

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

Equations

Instances For

instance Equiv.instTrans :

Trans Equiv Equiv Equiv

Equations

@[simp]

theorem Equiv.trans_def {a✝ : Sort u_2} {b✝ : Sort u_1} {c✝ : Sort u_3} (e₁ : a✝ ≃ b✝) (e₂ : b✝ ≃ c✝) :

Trans.trans e₁ e₂ = e₁.trans e₂

def Equiv.symmEquiv (α : Sort u_1) (β : Sort u_2) :

α ≃ β ≃ (β ≃ α)

Equiv.symm defines an equivalence between α ≃ β and β ≃ α.

Equations

Instances For

@[simp]

theorem Equiv.symmEquiv_symm_apply_symm_apply (α : Sort u_1) (β : Sort u_2) (e : β ≃ α) (a✝ : β) :

((symmEquiv α β).symm e).symm a✝ = e.toFun a✝

@[simp]

theorem Equiv.symmEquiv_symm_apply_apply (α : Sort u_1) (β : Sort u_2) (e : β ≃ α) (a✝ : α) :

((symmEquiv α β).symm e) a✝ = e.invFun a✝

@[simp]

theorem Equiv.symmEquiv_apply_apply (α : Sort u_1) (β : Sort u_2) (e : α ≃ β) (a✝ : β) :

((symmEquiv α β) e) a✝ = e.invFun a✝

@[simp]

theorem Equiv.symmEquiv_apply_symm_apply (α : Sort u_1) (β : Sort u_2) (e : α ≃ β) (a✝ : α) :

((symmEquiv α β) e).symm a✝ = e.toFun a✝

@[simp]

theorem Equiv.toFun_as_coe {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.toFun = ⇑e

@[simp]

theorem Equiv.invFun_as_coe {α : Sort u} {β : Sort v} (e : α ≃ β) :

e.invFun = ⇑e.symm

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

Function.Injective ⇑e

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

Function.Surjective ⇑e

theorem Equiv.bijective {α : Sort u} {β : Sort v} (e : α ≃ β) :

Function.Bijective ⇑e

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

Subsingleton α

theorem Equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton α] :

Subsingleton β

theorem Equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α ≃ β) :

Subsingleton α ↔ Subsingleton β

instance Equiv.equiv_subsingleton_cod {α : Sort u} {β : Sort v} [Subsingleton β] :

Subsingleton (α ≃ β)

instance Equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [Subsingleton α] :

Subsingleton (α ≃ β)

instance Equiv.permUnique {α : Sort u} [Subsingleton α] :

Unique (Perm α)

Equations

theorem Equiv.Perm.subsingleton_eq_refl {α : Sort u} [Subsingleton α] (e : Perm α) :

e = Equiv.refl α

theorem Equiv.nontrivial {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Nontrivial β] :

Nontrivial α

theorem Equiv.nontrivial_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

Nontrivial α ↔ Nontrivial β

@[reducible, inline]

abbrev Equiv.decidableEq {α : Sort u} {β : Sort v} (e : α ≃ β) [DecidableEq β] :

DecidableEq α

Transfer DecidableEq across an equivalence.

Equations

Instances For

theorem Equiv.nonempty_congr {α : Sort u} {β : Sort v} (e : α ≃ β) :

Nonempty α ↔ Nonempty β

theorem Equiv.nonempty {α : Sort u} {β : Sort v} (e : α ≃ β) [Nonempty β] :

Nonempty α

@[reducible, inline]

abbrev Equiv.inhabited {α : Sort u} {β : Sort v} [Inhabited β] (e : α ≃ β) :

Inhabited α

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

Equations

Instances For

@[reducible, inline]

abbrev Equiv.unique {α : Sort u} {β : Sort v} [Unique β] (e : α ≃ β) :

Unique α

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

Equations

Instances For

def Equiv.cast {α β : Sort u_1} (h : α = β) :

α ≃ β

Equivalence between equal types.

Equations

Instances For

@[simp]

theorem Equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) :

⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g

@[simp]

theorem Equiv.coe_refl {α : Sort u} :

⇑(Equiv.refl α) = id

theorem Equiv.Perm.coe_subsingleton {α : Type u_1} [Subsingleton α] (e : Perm α) :

⇑e = id

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

@[simp]

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

(Equiv.refl α) x = x

@[simp]

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

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

@[simp]

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

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

@[simp]

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

e (e.symm x) = x

@[simp]

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

e.symm (e x) = x

@[simp]

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

⇑e.symm ∘ ⇑e = id

@[simp]

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

⇑e ∘ ⇑e.symm = id

@[simp]

theorem EquivLike.apply_coe_symm_apply {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : β) :

e ((↑e).symm x) = x

@[simp]

theorem EquivLike.coe_symm_apply_apply {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : α) :

(↑e).symm (e x) = x

@[simp]

theorem EquivLike.coe_symm_comp_self {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) :

⇑(↑e).symm ∘ ⇑e = id

@[simp]

theorem EquivLike.self_comp_coe_symm {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) :

⇑e ∘ ⇑(↑e).symm = id

@[simp]

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

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

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

f.symm.symm b = f b

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

f x = f y ↔ x = y

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

f x = y ↔ x = f.symm y

@[simp]

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

(Equiv.cast h) x = cast h x

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

Equiv.cast ⋯ = (Equiv.cast h).symm

@[simp]

theorem Equiv.cast_refl {α : Sort u_1} (h : α = α := ⋯) :

Equiv.cast h = Equiv.refl α

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

Equiv.cast ⋯ = (Equiv.cast h).trans (Equiv.cast h2)

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

(Equiv.cast h) a = b ↔ a ≍ b

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

e.symm x = y ↔ x = e y

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

y = e.symm x ↔ e y = x

@[simp]

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

e.symm.symm = e

Function.Bijective Equiv.symm

theorem Equiv.symm_bijective {α : Sort u} {β : Sort v} :

@[simp]

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

e.trans (Equiv.refl β) = e

@[simp]

theorem Equiv.refl_symm {α : Sort u} :

(Equiv.refl α).symm = Equiv.refl α

@[simp]

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

(Equiv.refl α).trans e = e

@[simp]

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

e.symm.trans e = Equiv.refl β

@[simp]

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

e.trans e.symm = Equiv.refl α

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

(ab.trans bc).trans cd = ab.trans (bc.trans cd)

theorem Equiv.trans_cancel_left {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β ≃ γ) (g : α ≃ γ) :

e.trans f = g ↔ f = e.symm.trans g

theorem Equiv.trans_cancel_right {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β ≃ γ) (g : α ≃ γ) :

e.trans f = g ↔ e = g.trans f.symm

theorem Equiv.leftInverse_symm {α : Sort u} {β : Sort v} (f : α ≃ β) :

Function.LeftInverse ⇑f.symm ⇑f

theorem Equiv.rightInverse_symm {α : Sort u} {β : Sort v} (f : α ≃ β) :

Function.RightInverse ⇑f.symm ⇑f

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

Function.Injective (f ∘ ⇑e) ↔ Function.Injective f

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

Function.Injective (⇑e ∘ f) ↔ Function.Injective f

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

Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f

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

Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f

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

Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f

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

Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f

@[simp]

theorem Equiv.extend_apply {α : Sort u} {β : Sort v} {γ : Sort w} {f : α ≃ β} (g : α → γ) (e' : β → γ) (b : β) :

Function.extend (⇑f) g e' b = g (f.symm b)

def Equiv.equivCongr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) :

α ≃ γ ≃ (β ≃ δ)

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

Equations

Instances For

@[simp]

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

((ab.equivCongr cd) e) x = cd (e (ab.symm x))

@[simp]

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

(ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

@[simp]

theorem Equiv.equivCongr_refl {α : Sort u_1} {β : Sort u_2} :

(Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

@[simp]

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

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

@[simp]

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

((Equiv.refl α).equivCongr bg) e = e.trans bg

@[simp]

theorem Equiv.equivCongr_refl_right {α : Sort u_1} {β : Sort u_2} (ab e : α ≃ β) :

(ab.equivCongr (Equiv.refl β)) e = ab.symm.trans e

def Equiv.permCongr {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') :

Perm α' ≃ Perm β'

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

Equations

Instances For

theorem Equiv.permCongr_def {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Perm α') :

e.permCongr p = (e.symm.trans p).trans e

@[simp]

theorem Equiv.permCongr_refl {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') :

e.permCongr (Equiv.refl α') = Equiv.refl β'

@[simp]

theorem Equiv.permCongr_symm {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') :

e.permCongr.symm = e.symm.permCongr

@[simp]

theorem Equiv.permCongr_apply {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Perm α') (x : β') :

(e.permCongr p) x = e (p (e.symm x))

theorem Equiv.permCongr_symm_apply {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Perm β') (x : α') :

(e.permCongr.symm p) x = e.symm (p (e x))

theorem Equiv.permCongr_trans {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p p' : Perm α') :

Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')

def Equiv.equivOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] [IsEmpty β] :

α ≃ β

Two empty types are equivalent.

Equations

Instances For

def Equiv.equivEmpty (α : Sort u) [IsEmpty α] :

α ≃ Empty

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

Equations

Instances For

def Equiv.equivPEmpty (α : Sort v) [IsEmpty α] :

α ≃ PEmpty.{u}

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

Equations

Instances For

def Equiv.equivEmptyEquiv (α : Sort u) :

α ≃ Empty ≃ IsEmpty α

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

Equations

Instances For

def Equiv.propEquivPEmpty {p : Prop} (h : ¬p) :

p ≃ PEmpty.{u_1}

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

Equations

Instances For

def Equiv.ofUnique (α : Sort u) (β : Sort v) [Unique α] [Unique β] :

α ≃ β

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

Equations

Instances For

@[simp]

theorem Equiv.ofUnique_symm_apply (α : Sort u) (β : Sort v) [Unique α] [Unique β] (a✝ : β) :

(ofUnique α β).symm a✝ = default a✝

@[simp]

theorem Equiv.ofUnique_apply (α : Sort u) (β : Sort v) [Unique α] [Unique β] (a✝ : α) :

(ofUnique α β) a✝ = default a✝

def Equiv.equivPUnit (α : Sort u) [Unique α] :

α ≃ PUnit.{v}

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

Equations

Instances For

@[simp]

theorem Equiv.equivPUnit_symm_apply (α : Sort u) [Unique α] (a✝ : PUnit.{v}) :

(equivPUnit α).symm a✝ = default

@[simp]

theorem Equiv.equivPUnit_apply (α : Sort u) [Unique α] (a✝ : α) :

(equivPUnit α) a✝ = PUnit.unit

def Equiv.propEquivPUnit {p : Prop} (h : p) :

p ≃ PUnit.{0}

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

Equations

Instances For

def Equiv.ulift {α : Type v} :

ULift.{u, v} α ≃ α

ULift α is equivalent to α.

Equations

Instances For

@[simp]

theorem Equiv.ulift_symm_apply {α : Type v} :

⇑Equiv.ulift.symm = ULift.up

@[simp]

theorem Equiv.ulift_apply {α : Type v} :

⇑Equiv.ulift = ULift.down

def Equiv.plift {α : Sort u} :

PLift α ≃ α

PLift α is equivalent to α.

Equations

Instances For

@[simp]

theorem Equiv.plift_apply {α : Sort u} :

⇑Equiv.plift = PLift.down

@[simp]

theorem Equiv.plift_symm_apply {α : Sort u} :

⇑Equiv.plift.symm = PLift.up

def Equiv.ofIff {P Q : Prop} (h : P ↔ Q) :

P ≃ Q

equivalence of propositions is the same as iff

Equations

Instances For

def Equiv.arrowCongr {α₁ : 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

Instances For

@[simp]

theorem Equiv.arrowCongr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (f : α₁ → β₁) (a✝ : α₂) :

(e₁.arrowCongr e₂) f a✝ = (⇑e₂ ∘ f ∘ ⇑e₁.symm) a✝

theorem Equiv.arrowCongr_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.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f

@[simp]

theorem Equiv.arrowCongr_refl {α : Sort u_1} {β : Sort u_2} :

(Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (α → β)

@[simp]

theorem Equiv.arrowCongr_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₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')

@[simp]

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

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

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

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

A version of Equiv.arrowCongr in Type, rather than Sort.

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

Equations

Instances For

@[simp]

theorem Equiv.arrowCongr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) (f : α₁ → β₁) (a✝ : α₂) :

(hα.arrowCongr' hβ) f a✝ = hβ (f (hα.symm a✝))

@[simp]

theorem Equiv.arrowCongr'_refl {α : Type u_1} {β : Type u_2} :

(Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.refl (α → β)

@[simp]

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

@[simp]

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

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

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

(α → α) ≃ (β → β)

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

Equations

Instances For

@[simp]

theorem Equiv.conj_apply {α : Sort u} {β : Sort v} (e : α ≃ β) (f : α → α) (a✝ : β) :

e.conj f a✝ = e (f (e.symm a✝))

@[simp]

theorem Equiv.conj_refl {α : Sort u} :

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

@[simp]

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

e.conj.symm = e.symm.conj

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

theorem Equiv.trans_eq_refl_iff_eq_symm {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} :

f.trans g = Equiv.refl α ↔ f = g.symm

theorem Equiv.trans_eq_refl_iff_symm_eq {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} :

f.trans g = Equiv.refl α ↔ f.symm = g

theorem Equiv.eq_symm_iff_trans_eq_refl {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} :

f = g.symm ↔ f.trans g = Equiv.refl α

theorem Equiv.symm_eq_iff_trans_eq_refl {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} :

f.symm = g ↔ f.trans g = Equiv.refl α

def Equiv.punitEquivPUnit :

PUnit.{v} ≃ PUnit.{w}

PUnit sorts in any two universes are equivalent.

Equations

Instances For

noncomputable def Equiv.propEquivBool :

Prop ≃ Bool

Prop is noncomputably equivalent to Bool.

Equations

Instances For

def Equiv.arrowPUnitEquivPUnit (α : Sort u_1) :

(α → PUnit.{v}) ≃ PUnit.{w}

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

Equations

Instances For

def Equiv.piUnique {α : Sort u} [Unique α] (β : α → Sort u_1) :

((i : α) → β i) ≃ β default

The equivalence (∀ i, β i) ≃ β ⋆ when the domain of β only contains ⋆

Equations

Instances For

@[simp]

theorem Equiv.piUnique_symm_apply {α : Sort u} [Unique α] (β : α → Sort u_1) :

⇑(piUnique β).symm = uniqueElim

@[simp]

theorem Equiv.piUnique_apply {α : Sort u} [Unique α] (β : α → Sort u_1) :

⇑(piUnique β) = fun (f : (i : α) → β i) => f default

def Equiv.funUnique (α : Sort u) (β : Sort u_1) [Unique α] :

(α → β) ≃ β

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

Equations

Instances For

@[simp]

theorem Equiv.funUnique_apply (α : Sort u) (β : Sort u_1) [Unique α] :

⇑(funUnique α β) = fun (f : α → β) => f default

@[simp]

theorem Equiv.funUnique_symm_apply (α : Sort u) (β : Sort u_1) [Unique α] :

⇑(funUnique α β).symm = uniqueElim

def Equiv.punitArrowEquiv (α : Sort u_1) :

(PUnit.{u} → α) ≃ α

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

Equations

Instances For

def Equiv.trueArrowEquiv (α : Sort u_1) :

(True → α) ≃ α

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

Equations

Instances For

def Equiv.arrowPUnitOfIsEmpty (α : Sort u_1) (β : Sort u_2) [IsEmpty α] :

(α → β) ≃ PUnit.{u}

The sort of maps from a type that IsEmpty is equivalent to PUnit.

Equations

Instances For

def Equiv.emptyArrowEquivPUnit (α : Sort u_1) :

(Empty → α) ≃ PUnit.{u}

The sort of maps from Empty is equivalent to PUnit.

Equations

Instances For

def Equiv.pemptyArrowEquivPUnit (α : Sort u_1) :

(PEmpty.{u_2} → α) ≃ PUnit.{u}

The sort of maps from PEmpty is equivalent to PUnit.

Equations

Instances For

def Equiv.falseArrowEquivPUnit (α : Sort u_1) :

(False → α) ≃ PUnit.{u}

The sort of maps from False is equivalent to PUnit.

Equations

Instances For

def Equiv.psigmaEquivSigma {α : Type u_2} (β : α → Type u_1) :

(i : α) ×' β i ≃ (i : α) × β i

A PSigma-type is equivalent to the corresponding Sigma-type.

Equations

Instances For

@[simp]

theorem Equiv.psigmaEquivSigma_symm_apply {α : Type u_2} (β : α → Type u_1) (a : (i : α) × β i) :

(psigmaEquivSigma β).symm a = ⟨a.fst, a.snd⟩

@[simp]

theorem Equiv.psigmaEquivSigma_apply {α : Type u_2} (β : α → Type u_1) (a : (i : α) ×' β i) :

(psigmaEquivSigma β) a = ⟨a.fst, a.snd⟩

def Equiv.psigmaEquivSigmaPLift {α : Sort u_2} (β : α → Sort u_1) :

(i : α) ×' β i ≃ (i : PLift α) × PLift (β i.down)

A PSigma-type is equivalent to the corresponding Sigma-type.

Equations

Instances For

@[simp]

theorem Equiv.psigmaEquivSigmaPLift_apply {α : Sort u_2} (β : α → Sort u_1) (a : (i : α) ×' β i) :

(psigmaEquivSigmaPLift β) a = ⟨{ down := a.fst }, { down := a.snd }⟩

@[simp]

theorem Equiv.psigmaEquivSigmaPLift_symm_apply {α : Sort u_2} (β : α → Sort u_1) (a : (i : PLift α) × PLift (β i.down)) :

(psigmaEquivSigmaPLift β).symm a = ⟨a.fst.down, a.snd.down⟩

def Equiv.psigmaCongrRight {α : Sort u} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (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

Instances For

@[simp]

theorem Equiv.psigmaCongrRight_apply {α : Sort u} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a) (a : (a : α) ×' β₁ a) :

(psigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩

theorem Equiv.psigmaCongrRight_trans {α : Sort u_4} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} {β₃ : α → Sort u_3} (F : (a : α) → β₁ a ≃ β₂ a) (G : (a : α) → β₂ a ≃ β₃ a) :

(psigmaCongrRight F).trans (psigmaCongrRight G) = psigmaCongrRight fun (a : α) => (F a).trans (G a)

theorem Equiv.psigmaCongrRight_symm {α : Sort u_3} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a) :

(psigmaCongrRight F).symm = psigmaCongrRight fun (a : α) => (F a).symm

@[simp]

theorem Equiv.psigmaCongrRight_refl {α : Sort u_2} {β : α → Sort u_1} :

(psigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)

def Equiv.sigmaCongrRight {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (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

Instances For

@[simp]

theorem Equiv.sigmaCongrRight_apply {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) (a : (a : α) × β₁ a) :

(sigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩

theorem Equiv.sigmaCongrRight_trans {α : Type u_4} {β₁ : α → Type u_1} {β₂ : α → Type u_2} {β₃ : α → Type u_3} (F : (a : α) → β₁ a ≃ β₂ a) (G : (a : α) → β₂ a ≃ β₃ a) :

(sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun (a : α) => (F a).trans (G a)

theorem Equiv.sigmaCongrRight_symm {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) :

(sigmaCongrRight F).symm = sigmaCongrRight fun (a : α) => (F a).symm

@[simp]

theorem Equiv.sigmaCongrRight_refl {α : Type u_2} {β : α → Type u_1} :

(sigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)

def Equiv.psigmaEquivSubtype {α : Type v} (P : α → Prop) :

(i : α) ×' P i ≃ Subtype P

A PSigma with Prop fibers is equivalent to the subtype.

Equations

Instances For

def Equiv.sigmaPLiftEquivSubtype {α : Type v} (P : α → Prop) :

(i : α) × PLift (P i) ≃ Subtype P

A Sigma with PLift fibers is equivalent to the subtype.

Equations

Instances For

def Equiv.sigmaULiftPLiftEquivSubtype {α : Type v} (P : α → Prop) :

(i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P

A Sigma with fun i ↦ ULift (PLift (P i)) fibers is equivalent to { x // P x }. Variant of sigmaPLiftEquivSubtype.

Equations

Instances For

@[reducible, inline]

abbrev Equiv.Perm.sigmaCongrRight {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Perm (β a)) :

Perm ((a : α) × β a)

A family of permutations Π a, Perm (β a) generates a permutation Perm (Σ a, β₁ a).

Equations

Instances For

@[simp]

theorem Equiv.Perm.sigmaCongrRight_trans {α : Type u_1} {β : α → Type u_2} (F G : (a : α) → Perm (β a)) :

Equiv.trans (sigmaCongrRight F) (sigmaCongrRight G) = sigmaCongrRight fun (a : α) => Equiv.trans (F a) (G a)

@[simp]

theorem Equiv.Perm.sigmaCongrRight_symm {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Perm (β a)) :

Equiv.symm (sigmaCongrRight F) = sigmaCongrRight fun (a : α) => Equiv.symm (F a)

@[simp]

theorem Equiv.Perm.sigmaCongrRight_refl {α : Type u_1} {β : α → Type u_2} :

(sigmaCongrRight fun (a : α) => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)

def Equiv.functionSwap (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) :

((a : α) → (b : β) → γ a b) ≃ ((b : β) → (a : α) → γ a b)

Function.swap as an equivalence.

Equations

Instances For

@[simp]

theorem Equiv.functionSwap_apply (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) :

⇑(functionSwap α β γ) = Function.swap

@[simp]

theorem Equiv.functionSwap_symm_apply (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) :

⇑(functionSwap α β γ).symm = Function.swap

theorem Function.swap_bijective {α : Sort u_1} {β : Sort u_2} {γ : α → β → Sort u_3} :

Bijective swap

def Equiv.sigmaCongrLeft {α₁ : 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

Instances For

@[simp]

theorem Equiv.sigmaCongrLeft_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) (a : (a : α₁) × β (e a)) :

e.sigmaCongrLeft a = ⟨e a.fst, a.snd⟩

def Equiv.sigmaCongrLeft' {α₁ : 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

Instances For

def Equiv.sigmaCongr {α₁ : 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

Instances For

def Equiv.sigmaEquivProd (α : Type u_1) (β : Type u_2) :

(_ : α) × β ≃ α × β

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

Equations

Instances For

@[simp]

theorem Equiv.sigmaEquivProd_apply (α : Type u_1) (β : Type u_2) (a : (_ : α) × β) :

(sigmaEquivProd α β) a = (a.fst, a.snd)

@[simp]

theorem Equiv.sigmaEquivProd_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :

(sigmaEquivProd α β).symm a = ⟨a.1, a.2⟩

def Equiv.sigmaEquivProdOfEquiv {α : 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

Instances For

def Equiv.sigmaAssoc {α : Type u_1} {β : α → Type u_2} (γ : (a : α) → β a → Type u_3) :

(ab : (a : α) × β a) × γ ab.fst ab.snd ≃ (a : α) × (b : β a) × γ a b

The dependent product of types is associative up to an equivalence.

Equations

Instances For

def Equiv.pSigmaAssoc {α : Sort u_1} {β : α → Sort u_2} (γ : (a : α) → β a → Sort u_3) :

(ab : (a : α) ×' β a) ×' γ ab.fst ab.snd ≃ (a : α) ×' (b : β a) ×' γ a b

The dependent product of sorts is associative up to an equivalence.

Equations

Instances For

theorem Equiv.forall_congr_right {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) :

(∀ (a : α), q (e a)) ↔ ∀ (b : β), q b

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

(∀ (a : α), p a) ↔ ∀ (b : β), p (e.symm b)

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

(∀ (a : α), p a) ↔ ∀ (b : β), q b

theorem Equiv.forall_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) :

(∀ (a : α), p a) ↔ ∀ (b : β), q b

theorem Equiv.exists_congr_right {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) :

(∃ (a : α), q (e a)) ↔ ∃ (b : β), q b

theorem Equiv.exists_congr_left {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) :

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

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

(∃ (a : α), p a) ↔ ∃ (b : β), q b

theorem Equiv.exists_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) :

(∃ (a : α), p a) ↔ ∃ (b : β), q b

theorem Equiv.exists_subtype_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : { a : α // p a } ≃ { b : β // q b }) :

(∃ (a : α), p a) ↔ ∃ (b : β), q b

theorem Equiv.existsUnique_congr_right {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) :

(∃! a : α, q (e a)) ↔ ∃! b : β, q b

theorem Equiv.existsUnique_congr_left {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) :

(∃! a : α, p a) ↔ ∃! b : β, p (e.symm b)

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

(∃! a : α, p a) ↔ ∃! b : β, q b

theorem Equiv.existsUnique_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) :

(∃! a : α, p a) ↔ ∃! b : β, q b

theorem Equiv.existsUnique_subtype_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : { a : α // p a } ≃ { b : β // q b }) :

(∃! a : α, p a) ↔ ∃! b : β, q b

theorem Equiv.forall₂_congr {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {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

theorem Equiv.forall₂_congr' {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {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

theorem Equiv.forall₃_congr {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {γ₁ : Sort u_5} {γ₂ : Sort u_6} {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

theorem Equiv.forall₃_congr' {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {γ₁ : Sort u_5} {γ₂ : Sort u_6} {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

noncomputable def Equiv.ofBijective {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) :

α ≃ β

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

Equations

Instances For

@[simp]

theorem Equiv.ofBijective_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (a✝ : α) :

(ofBijective f hf) a✝ = f a✝

theorem Equiv.ofBijective_apply_symm_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : β) :

f ((ofBijective f hf).symm x) = x

@[simp]

theorem Equiv.ofBijective_symm_apply_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : α) :

(ofBijective f hf).symm (f x) = x

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

Instances For

@[simp]

theorem Quot.congr_mk {α : Sort u} {β : Sort v} {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :

(Quot.congr e eq) (mk ra a) = mk rb (e a)

def Quot.congrRight {α : 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

Instances For

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

Quot r ≃ Quot fun (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

Instances For

def Quotient.congr {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (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

Instances For

@[simp]

theorem Quotient.congr_mk {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :

(Quotient.congr e eq) ⟦a⟧ = ⟦e a⟧

def Quotient.congrRight {α : Sort u} {r r' : Setoid α} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ ↔ 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

Instances For

def finZeroEquiv :

Fin 0 ≃ Empty

Equivalence between Fin 0 and Empty.

Equations

Instances For