# mathlibdocumentation

logic.equiv.basic

# Equivalence between types #

In this file we define two types:

• `equiv α β` a.k.a. `α ≃ β`: a bijective map `α → β` bundled with its inverse map; we use this (and not equality!) to express that various `Type`s or `Sort`s are equivalent.

• `equiv.perm α`: the group of permutations `α ≃ α`. More lemmas about `equiv.perm` can be found in `group_theory/perm`.

Then we define

• canonical isomorphisms between various types: e.g.,

• `equiv.refl α` is the identity map interpreted as `α ≃ α`;

• `equiv.sum_equiv_sigma_bool` is the canonical equivalence between the sum of two types `α ⊕ β` and the sigma-type `Σ b : bool, cond b α β`;

• `equiv.prod_sum_distrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)` shows that type product and type sum satisfy the distributive law up to a canonical equivalence;

• operations on equivalences: e.g.,

• `equiv.symm e : β ≃ α` is the inverse of `e : α ≃ β`;

• `equiv.trans e₁ e₂ : α ≃ γ` is the composition of `e₁ : α ≃ β` and `e₂ : β ≃ γ` (note the order of the arguments!);

• `equiv.prod_congr ea eb : α₁ × β₁ ≃ α₂ × β₂`: combine two equivalences `ea : α₁ ≃ α₂` and `eb : β₁ ≃ β₂` using `prod.map`.

• definitions that transfer some instances along an equivalence. By convention, we transfer instances from right to left.

• `equiv.inhabited` takes `e : α ≃ β` and `[inhabited β]` and returns `inhabited α`;
• `equiv.unique` takes `e : α ≃ β` and `[unique β]` and returns `unique α`;
• `equiv.decidable_eq` takes `e : α ≃ β` and `[decidable_eq β]` and returns `decidable_eq α`.

More definitions of this kind can be found in other files. E.g., `data/equiv/transfer_instance` does it for many algebraic type classes like `group`, `module`, etc.

## Tags #

equivalence, congruence, bijective map

@[nolint]
structure equiv (α : Sort u_1) (β : Sort u_2) :
Sort (max 1 (imax u_1 u_2) (imax u_2 u_1))
• to_fun : α → β
• inv_fun : β → α
• left_inv : self.to_fun
• right_inv : self.to_fun

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

Instances for `equiv`
@[protected, instance]
def equiv.has_coe_t {α : Sort u} {β : Sort v} {F : Sort u_1} [ α β] :
β)
Equations
def equiv.perm (α : Sort u_1) :
Sort (max 1 u_1)

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

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

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

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

Any type is equivalent to itself.

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

Inverse of an equivalence `e : α ≃ β`.

Equations
def equiv.simps.symm_apply {α : Sort u} {β : Sort v} (e : α β) :
β → α
Equations
@[protected]
def equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
α γ

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

Equations
@[simp]
theorem equiv.to_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.inv_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.injective {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.surjective {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.bijective {α : Sort u} {β : Sort v} (e : α β) :
@[protected]
theorem equiv.subsingleton {α : Sort u} {β : Sort v} (e : α β) [subsingleton β] :
@[protected]
theorem equiv.subsingleton.symm {α : Sort u} {β : Sort v} (e : α β) [subsingleton α] :
theorem equiv.subsingleton_congr {α : Sort u} {β : Sort v} (e : α β) :
@[protected, instance]
def equiv.equiv_subsingleton_cod {α : Sort u} {β : Sort v} [subsingleton β] :
@[protected, instance]
def equiv.equiv_subsingleton_dom {α : Sort u} {β : Sort v} [subsingleton α] :
@[protected, instance]
def equiv.perm_unique {α : Sort u} [subsingleton α] :
Equations
theorem equiv.perm.subsingleton_eq_refl {α : Sort u} [subsingleton α] (e : equiv.perm α) :
e =
@[protected]
def equiv.decidable_eq {α : Sort u} {β : Sort v} (e : α β) [decidable_eq β] :

Transfer `decidable_eq` across an equivalence.

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

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

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

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

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

Equivalence between equal types.

Equations
@[simp]
theorem equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : f) (r : f) :
({to_fun := f, inv_fun := g, left_inv := l, right_inv := r}.symm) = g
@[simp]
theorem equiv.coe_refl {α : Sort u} :
@[simp]
theorem equiv.perm.coe_subsingleton {α : Type u_1} [subsingleton α] (e : equiv.perm α) :
theorem equiv.refl_apply {α : Sort u} (x : α) :
(equiv.refl α) x = x
@[simp]
theorem equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) :
(f.trans g) = g f
theorem equiv.trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : α) :
(f.trans g) a = g (f a)
@[simp]
theorem equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α β) (x : β) :
e ((e.symm) x) = x
@[simp]
theorem equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
(e.symm) (e x) = x
@[simp]
theorem equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : γ) :
((f.trans g).symm) a = (f.symm) ((g.symm) a)
@[simp, nolint]
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_1} {β : Sort u_2} (f : α β) {x : α} {y : β} :
f x = y x = (f.symm) y
@[simp]
theorem equiv.cast_apply {α β : Sort u_1} (h : α = β) (x : α) :
(equiv.cast h) x = cast h x
@[simp]
theorem equiv.cast_symm {α β : Sort u_1} (h : α = β) :
@[simp]
theorem equiv.cast_refl {α : Sort u_1} (h : α = α := rfl) :
@[simp]
theorem equiv.cast_trans {α β γ : Sort u_1} (h : α = β) (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
@[simp]
theorem equiv.trans_refl {α : Sort u} {β : Sort v} (e : α β) :
e.trans (equiv.refl β) = e
@[simp]
theorem equiv.refl_symm {α : Sort u} :
@[simp]
theorem equiv.refl_trans {α : Sort u} {β : Sort v} (e : α β) :
(equiv.refl α).trans e = e
@[simp]
theorem equiv.symm_trans_self {α : Sort u} {β : Sort v} (e : α β) :
e.symm.trans e =
@[simp]
theorem equiv.self_trans_symm {α : Sort u} {β : Sort v} (e : α β) :
e.trans e.symm =
theorem equiv.trans_assoc {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (bc : β γ) (cd : γ δ) :
(ab.trans bc).trans cd = ab.trans (bc.trans cd)
theorem equiv.left_inverse_symm {α : Sort u} {β : Sort v} (f : α β) :
theorem equiv.right_inverse_symm {α : Sort u} {β : Sort v} (f : α β) :
theorem equiv.injective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : β → γ) :
theorem equiv.comp_injective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β γ) :
theorem equiv.surjective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : β → γ) :
theorem equiv.comp_surjective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β γ) :
theorem equiv.bijective_comp {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : β → γ) :
theorem equiv.comp_bijective {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β γ) :
def equiv.equiv_congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
α γ δ)

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

Equations
@[simp]
theorem equiv.equiv_congr_refl {α : Sort u_1} {β : Sort u_2} :
(equiv.refl β) = equiv.refl β)
@[simp]
theorem equiv.equiv_congr_symm {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (cd : γ δ) :
@[simp]
theorem equiv.equiv_congr_trans {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α β) (de : δ ε) (bc : β γ) (ef : ε ζ) :
(ab.equiv_congr de).trans (bc.equiv_congr ef) = (ab.trans bc).equiv_congr (de.trans ef)
@[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
@[simp]
theorem equiv.equiv_congr_refl_right {α : Sort u_1} {β : Sort u_2} (ab e : α β) :
@[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))
def equiv.perm_congr {α' : Type u_1} {β' : Type u_2} (e : α' β') :

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

Equations
theorem equiv.perm_congr_def {α' : Type u_1} {β' : Type u_2} (e : α' β') (p : equiv.perm α') :
@[simp]
theorem equiv.perm_congr_refl {α' : Type u_1} {β' : Type u_2} (e : α' β') :
@[simp]
theorem equiv.perm_congr_symm {α' : Type u_1} {β' : Type u_2} (e : α' β') :
@[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))
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))
theorem equiv.perm_congr_trans {α' : Type u_1} {β' : Type u_2} (e : α' β') (p p' : equiv.perm α') :
def equiv.equiv_of_is_empty (α : Sort u_1) (β : Sort u_2) [is_empty α] [is_empty β] :
α β

Two empty types are equivalent.

Equations
def equiv.equiv_empty (α : Sort u) [is_empty α] :

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

Equations
def equiv.equiv_pempty (α : Sort v) [is_empty α] :

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

Equations
def equiv.equiv_empty_equiv (α : Sort u) :

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

Equations
def equiv.prop_equiv_pempty {p : Prop} (h : ¬p) :

The `Sort` of proofs of a false proposition is equivalent to `pempty`.

Equations
def equiv.equiv_of_unique (α : Sort u_1) (β : Sort u_2) [unique α] [unique β] :
α β

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

Equations
def equiv.equiv_punit (α : Sort u_1) [unique α] :

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

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

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

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

`ulift α` is equivalent to `α`.

Equations
@[simp]
theorem equiv.ulift_apply {α : Type v} :
@[simp]
theorem equiv.plift_apply {α : Sort u} :
@[protected]
def equiv.plift {α : Sort u} :
α

`plift α` is equivalent to `α`.

Equations
@[simp]
theorem equiv.plift_symm_apply {α : Sort u} :
(equiv.plift.symm) = plift.up
@[simp]
theorem equiv.pprod_equiv_prod_symm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :
= x.fst, x.snd
@[simp]
theorem equiv.pprod_equiv_prod_apply {α : Type u_1} {β : Type u_2} (x : β) :
= (x.fst, x.snd)
def equiv.pprod_equiv_prod {α : Type u_1} {β : Type u_2} :
β α × β

`pprod α β` is equivalent to `α × β`

Equations
@[simp]
theorem equiv.pprod_equiv_prod_plift_symm_apply {α : Sort u_1} {β : Sort u_2} (x : × ) :
= x.fst.down, x.snd.down
def equiv.pprod_equiv_prod_plift {α : Sort u_1} {β : Sort u_2} :
β ×

`pprod α β` is equivalent to `plift α × plift β`

Equations
@[simp]
theorem equiv.pprod_equiv_prod_plift_apply {α : Sort u_1} {β : Sort u_2} (x : β) :
= ({down := x.fst}, {down := x.snd})
def equiv.of_iff {P Q : Prop} (h : P Q) :
P Q

equivalence of propositions is the same as iff

Equations
@[simp]
theorem equiv.arrow_congr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁ → β₁) (ᾰ : α₂) :
(e₁.arrow_congr e₂) f = (e₂ f (e₁.symm))
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
theorem equiv.arrow_congr_comp {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :
(ea.arrow_congr ec) (g f) = (eb.arrow_congr ec) g (ea.arrow_congr eb) f
@[simp]
theorem equiv.arrow_congr_refl {α : Sort u_1} {β : Sort u_2} :
(equiv.refl β) = equiv.refl (α → β)
@[simp]
theorem equiv.arrow_congr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).arrow_congr (e₁'.trans e₂') = (e₁.arrow_congr e₁').trans (e₂.arrow_congr e₂')
@[simp]
theorem equiv.arrow_congr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.arrow_congr e₂).symm = e₁.symm.arrow_congr e₂.symm
def equiv.arrow_congr' {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (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
@[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 = (f ((hα.symm) ᾰ))
@[simp]
theorem equiv.arrow_congr'_refl {α : Type u_1} {β : Type u_2} :
(equiv.refl β) = equiv.refl (α → β)
@[simp]
theorem equiv.arrow_congr'_trans {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).arrow_congr' (e₁'.trans e₂') = (e₁.arrow_congr' e₁').trans (e₂.arrow_congr' e₂')
@[simp]
theorem equiv.arrow_congr'_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.arrow_congr' e₂).symm = e₁.symm.arrow_congr' e₂.symm
def equiv.conj {α : Sort u} {β : Sort v} (e : α β) :
(α → α) (β → β)

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

Equations
@[simp]
theorem equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : α → α) (ᾰ : β) :
(e.conj) f = e (f ((e.symm) ᾰ))
@[simp]
theorem equiv.conj_refl {α : Sort u} :
(equiv.refl α).conj = equiv.refl (α → α)
@[simp]
theorem equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :
@[simp]
theorem equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
(e₁.trans e₂).conj = e₁.conj.trans e₂.conj
theorem equiv.conj_comp {α : Sort u} {β : Sort v} (e : α β) (f₁ f₂ : α → α) :
(e.conj) (f₁ f₂) = (e.conj) f₁ (e.conj) f₂
theorem equiv.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.semiconj_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁) :
((e.conj) f)
theorem equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) :
((e.arrow_congr e.conj) f)
@[protected, instance]
def equiv.arrow_congr.is_associative {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :
@[protected, instance]
def equiv.arrow_congr.is_idempotent {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :
@[protected, instance]
def equiv.arrow_congr.is_left_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :
@[protected, instance]
def equiv.arrow_congr.is_right_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :

`punit` sorts in any two universes are equivalent.

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

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

Equations
def equiv.Pi_subsingleton {α : Sort u_1} (β : α → Sort u_2) [subsingleton α] (a : α) :
(Π (a' : α), β a') β a

If `α` is `subsingleton` and `a : α`, then the type of dependent functions `Π (i : α), β i` is equivalent to `β i`.

Equations
@[simp]
theorem equiv.Pi_subsingleton_symm_apply {α : Sort u_1} (β : α → Sort u_2) [subsingleton α] (a : α) (x : β a) (b : α) :
a).symm) x b = cast _ x
@[simp]
theorem equiv.Pi_subsingleton_apply {α : Sort u_1} (β : α → Sort u_2) [subsingleton α] (a : α) (f : Π (x : α), (λ (a' : α), β a') x) :
f =
def equiv.fun_unique (α : Sort u_1) (β : Sort u_2) [unique α] :
(α → β) β

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

Equations
@[simp]
theorem equiv.fun_unique_symm_apply (α : Sort u_1) (β : Sort u_2) [unique α] :
β).symm) = λ (x : β) (b : α), x
@[simp]
theorem equiv.fun_unique_apply (α : Sort u_1) (β : Sort u_2) [unique α] :
def equiv.punit_arrow_equiv (α : Sort u_1) :
(punit → α) α

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

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

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

Equations
def equiv.arrow_punit_of_is_empty (α : Sort u_1) (β : Sort u_2) [is_empty α] :
(α → β) punit

The sort of maps from a type that `is_empty` is equivalent to `punit`.

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

The sort of maps from `empty` is equivalent to `punit`.

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

The sort of maps from `pempty` is equivalent to `punit`.

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

The sort of maps from `false` is equivalent to `punit`.

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

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

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

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

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

Type product is associative up to an equivalence.

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

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

Equations
@[simp]
theorem equiv.curry_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
def equiv.prod_punit (α : Type u_1) :
α

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

Equations
@[simp]
theorem equiv.prod_punit_apply (α : Type u_1) (p : α × punit) :
p = p.fst
@[simp]
theorem equiv.prod_punit_symm_apply (α : Type u_1) (a : α) :
def equiv.punit_prod (α : Type u_1) :
α

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

Equations
@[simp]
theorem equiv.punit_prod_symm_apply (α : Type u_1) (ᾰ : α) :
@[simp]
theorem equiv.punit_prod_apply (α : Type u_1) (ᾰ : punit × α) :
= ᾰ.snd
def equiv.prod_unique (α : Type u_1) (β : Type u_2) [unique β] :
α × β α

Any `unique` type is a right identity for type product up to equivalence.

Equations
def equiv.unique_prod (α : Type u_1) (β : Type u_2) [unique β] :
β × α α

Any `unique` type is a left identity for type product up to equivalence.

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

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

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

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

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

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

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

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

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

`psum` is equivalent to `sum`.

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

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

Equations
@[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)
@[simp]
theorem equiv.sum_congr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α β) (f : γ δ) :
@[simp]
theorem equiv.sum_congr_refl {α : Type u_1} {β : Type u_2} :
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
@[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
@[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 β) :
@[simp]
theorem equiv.perm.sum_congr_symm {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (f : equiv.perm β) :
@[simp]
theorem equiv.perm.sum_congr_refl {α : Type u_1} {β : Type u_2} :
= equiv.refl β)

`bool` is equivalent the sum of two `punit`s.

Equations
noncomputable def equiv.Prop_equiv_bool  :
Prop bool

`Prop` is noncomputably equivalent to `bool`.

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

Sum of types is commutative up to an equivalence.

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

Sum of types is associative up to an equivalence.

Equations
@[simp]
theorem equiv.sum_assoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
β γ) (sum.inl (sum.inl a)) =
@[simp]
theorem equiv.sum_assoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
β γ) (sum.inl (sum.inr b)) = sum.inr (sum.inl b)
@[simp]
theorem equiv.sum_assoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
β γ) (sum.inr c) = sum.inr (sum.inr c)
@[simp]
theorem equiv.sum_assoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
β γ).symm) (sum.inl a) = sum.inl (sum.inl a)
@[simp]
theorem equiv.sum_assoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
β γ).symm) (sum.inr (sum.inl b)) = sum.inl (sum.inr b)
@[simp]
theorem equiv.sum_assoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
β γ).symm) (sum.inr (sum.inr c)) =
def equiv.sum_empty (α : Type u_1) (β : Type u_2) [is_empty β] :
α β α

Sum with `empty` is equivalent to the original type.

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

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

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

`option α` is equivalent to `α ⊕ punit`

Equations
@[simp]
theorem equiv.option_equiv_sum_punit_none {α : Type u_1} :
@[simp]
theorem equiv.option_equiv_sum_punit_some {α : Type u_1} (a : α) :
@[simp]
theorem equiv.option_equiv_sum_punit_coe {α : Type u_1} (a : α) :
@[simp]
theorem equiv.option_equiv_sum_punit_symm_inl {α : Type u_1} (a : α) :
(sum.inl a) = a
@[simp]
theorem equiv.option_equiv_sum_punit_symm_inr {α : Type u_1} (a : punit) :
@[simp]
theorem equiv.option_is_some_equiv_symm_apply_coe (α : Type u_1) (x : α) :
( x) =
@[simp]
theorem equiv.option_is_some_equiv_apply (α : Type u_1) (o : {x // (x.is_some)}) :
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
@[simp]
theorem equiv.pi_option_equiv_prod_apply {α : Type u_1} {β : Type u_2} (f : Π (a : option α), β a) :
= , λ (a : α), f (option.some a))
@[simp]
theorem equiv.pi_option_equiv_prod_symm_apply {α : Type u_1} {β : Type u_2} (x : × Π (a : α), β (option.some a)) (a : option α) :
= a.cases_on x.fst x.snd
def equiv.pi_option_equiv_prod {α : Type u_1} {β : Type u_2} :
(Π (a : option α), β a) × Π (a : α), β (option.some a)

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

Equations
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
@[simp]
theorem equiv.sigma_fiber_equiv_apply {α : Type u_1} {β : Type u_2} (f : α → β) (x : Σ (y : β), {x // f x = y}) :
= (x.snd)
@[simp]
theorem equiv.sigma_fiber_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
((.symm) x).snd) = x
@[simp]
theorem equiv.sigma_fiber_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
(.symm) x).fst = f x
def equiv.sigma_fiber_equiv {α : Type u_1} {β : Type u_2} (f : α → β) :
(Σ (y : β), {x // f x = y}) α

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

Equations
def equiv.sum_compl {α : Type u_1} (p : α → Prop)  :
{a // p a} {a // ¬p a} α

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

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

Equations
@[simp]
theorem equiv.sum_compl_apply_inl {α : Type u_1} (p : α → Prop) (x : {a // p a}) :
@[simp]
theorem equiv.sum_compl_apply_inr {α : Type u_1} (p : α → Prop) (x : {a // ¬p a}) :
@[simp]
theorem equiv.sum_compl_apply_symm_of_pos {α : Type u_1} (p : α → Prop) (a : α) (h : p a) :
@[simp]
theorem equiv.sum_compl_apply_symm_of_neg {α : Type u_1} (p : α → Prop) (a : α) (h : ¬p a) :
def equiv.subtype_congr {α : Type u_1} {p q : α → Prop} (e : {x // p x} {x // q x}) (f : {x // ¬p x} {x // ¬q x}) :

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

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

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

Equations
theorem equiv.perm.subtype_congr.apply {ε : Type u_1} {p : ε → Prop} (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⟩))
@[simp]
theorem equiv.perm.subtype_congr.left_apply {ε : Type u_1} {p : ε → Prop} (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : p a) :
(ep.subtype_congr en) a = (ep a, h⟩)
@[simp]
theorem equiv.perm.subtype_congr.left_apply_subtype {ε : Type u_1} {p : ε → Prop} (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : {a // p a}) :
(ep.subtype_congr en) a = (ep a)
@[simp]
theorem equiv.perm.subtype_congr.right_apply {ε : Type u_1} {p : ε → Prop} (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) {a : ε} (h : ¬p a) :
(ep.subtype_congr en) a = (en a, h⟩)
@[simp]
theorem equiv.perm.subtype_congr.right_apply_subtype {ε : Type u_1} {p : ε → Prop} (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) (a : {a // ¬p a}) :
(ep.subtype_congr en) a = (en a)
@[simp]
theorem equiv.perm.subtype_congr.refl {ε : Type u_1} {p : ε → Prop}  :
@[simp]
theorem equiv.perm.subtype_congr.symm {ε : Type u_1} {p : ε → Prop} (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :
@[simp]
theorem equiv.perm.subtype_congr.trans {ε : Type u_1} {p : ε → Prop} (ep ep' : equiv.perm {a // p a}) (en en' : equiv.perm {a // ¬p a}) :
@[simp]
theorem equiv.subtype_preimage_symm_apply_coe {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) :
( x₀).symm) x) a = dite (p a) (λ (h : p a), x₀ a, h⟩) (λ (h : ¬p a), x a, h⟩)
@[simp]
theorem equiv.subtype_preimage_apply {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {x // x coe = x₀}) (a : {a // ¬p a}) :
x₀) x a = x a
def equiv.subtype_preimage {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) :
{x // x coe = x₀} ({a // ¬p a} → β)

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

Equations
theorem equiv.subtype_preimage_symm_apply_coe_pos {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) (h : p a) :
( x₀).symm) x) a = x₀ a, h⟩
theorem equiv.subtype_preimage_symm_apply_coe_neg {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) (h : ¬p a) :
( x₀).symm) x) a = x a, h⟩
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
def equiv.Pi_comm {α : Sort u_1} {β : Sort u_2} (φ : α → β → Sort u_3) :
(Π (a : α) (b : β), φ a b) Π (b : β) (a : α), φ a b

Given `φ : α → β → Sort*`, we have an equivalence between `Π a b, φ a b` and `Π b a, φ a b`. This is `function.swap` as an `equiv`.

Equations
@[simp]
theorem equiv.Pi_comm_apply {α : Sort u_1} {β : Sort u_2} (φ : α → β → Sort u_3) (f : Π (x : α) (y : β), (λ (a : α) (b : β), φ a b) x y) (y : β) (x : α) :
f y x = x
@[simp]
theorem equiv.Pi_comm_symm {α : Sort u_1} {β : Sort u_2} {φ : α → β → Sort u_3} :
def equiv.Pi_curry {α : Type u_1} {β : α → Type u_2} (γ : Π (a : α), β aType 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
def equiv.psigma_equiv_sigma {α : Type u_1} (β : α → Type u_2) :
(Σ' (i : α), β i) Σ (i : α), β i

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

Equations
@[simp]
theorem equiv.psigma_equiv_sigma_symm_apply {α : Type u_1} (β : α → Type u_2) (a : Σ (i : α), β i) :
a = a.fst, a.snd
@[simp]
theorem equiv.psigma_equiv_sigma_apply {α : Type u_1} (β : α → Type u_2) (a : Σ' (i : α), β i) :
= a.fst, a.snd
def equiv.psigma_equiv_sigma_plift {α : Sort u_1} (β : α → Sort u_2) :
(Σ' (i : α), β i) Σ (i : plift α), plift (β i.down)

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

Equations
@[simp]
theorem equiv.psigma_equiv_sigma_plift_apply {α : Sort u_1} (β : α → Sort u_2) (a : Σ' (i : α), β i) :
= {down := a.fst}, {down := a.snd}
@[simp]
theorem equiv.psigma_equiv_sigma_plift_symm_apply {α : Sort u_1} (β : α → Sort u_2) (a : Σ (i : plift α), plift (β i.down)) :
= a.fst.down, a.snd.down
@[simp]
theorem equiv.psigma_congr_right_apply {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ' (a : α), β₁ a) :
= a.fst, (F a.fst) a.snd
def equiv.psigma_congr_right {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (F : Π (a : α), β₁ a β₂ a) :
(Σ' (a : α), β₁ a) Σ' (a : α), β₂ a

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

Equations
@[simp]
theorem equiv.psigma_congr_right_trans {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} {β₃ : α → Sort u_4} (F : Π (a : α), β₁ a β₂ a) (G : Π (a : α), β₂ a β₃ a) :
= equiv.psigma_congr_right (λ (a : α), (F a).trans (G a))
@[simp]
theorem equiv.psigma_congr_right_symm {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} (F : Π (a : α), β₁ a β₂ a) :
= equiv.psigma_congr_right (λ (a : α), (F a).symm)
@[simp]
theorem equiv.psigma_congr_right_refl {α : Sort u_1} {β : α → Sort u_2} :
equiv.psigma_congr_right (λ (a : α), equiv.refl (β a)) = equiv.refl (Σ' (a : α), β a)
@[simp]
theorem equiv.sigma_congr_right_apply {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ (a : α), β₁ a) :
= a.fst, (F a.fst) a.snd
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
@[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 (λ (a : α), (F a).trans (G a))
@[simp]
theorem equiv.sigma_congr_right_symm {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a β₂ a) :
= equiv.sigma_congr_right (λ (a : α), (F a).symm)
@[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)
def equiv.psigma_equiv_subtype {α : Type v} (P : α → Prop) :
(Σ' (i : α), P i)

A `psigma` with `Prop` fibers is equivalent to the subtype.

Equations
def equiv.sigma_plift_equiv_subtype {α : Type v} (P : α → Prop) :
(Σ (i : α), plift (P i))

A `sigma` with `plift` fibers is equivalent to the subtype.

Equations
def equiv.sigma_ulift_plift_equiv_subtype {α : Type v} (P : α → Prop) :
(Σ (i : α), ulift (plift (P i)))

A `sigma` with `λ i, ulift (plift (P i))` fibers is equivalent to `{ x // P x }`. Variant of `sigma_plift_equiv_subtype`.

Equations
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
@[simp]
theorem equiv.perm.sigma_congr_right_trans {α : Type u_1} {β : α → Type u_2} (F G : Π (a : α), equiv.perm (β a)) :
= equiv.perm.sigma_congr_right (λ (a : α), equiv.trans (F a) (G a))
@[simp]
theorem equiv.perm.sigma_congr_right_symm {α : Type u_1} {β : α → Type u_2} (F : Π (a : α), equiv.perm (β a)) :
@[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)
@[simp]
theorem equiv.sigma_congr_left_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ α₂) (a : Σ (a : α₁), β (e a)) :
def equiv.sigma_congr_left {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ α₂) :
(Σ (a : α₁), β (e a)) Σ (a : α₂), β a

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

Equations
def equiv.sigma_congr_left' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ → Type u_3} (f : α₁ α₂) :
(Σ (a : α₁), β a) Σ (a : α₂), β ((f.symm) a)

Transporting a sigma type through an equivalence of the base

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

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

Equations
def equiv.sigma_equiv_prod (α : Type u_1) (β : Type u_2) :
(Σ (_x : α), β) α × β

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

Equations
@[simp]
theorem equiv.sigma_equiv_prod_apply (α : Type u_1) (β : Type u_2) (a : Σ (_x : α), β) :
a = (a.fst, a.snd)
@[simp]
theorem equiv.sigma_equiv_prod_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :
β).symm) a = a.fst, a.snd
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
def equiv.sigma_assoc {α : Type u_1} {β : α → Type u_2} (γ : Π (a : α), β aType u_3) :
(Σ (ab : Σ (a : α), β a), γ ab.fst ab.snd) Σ (a : α) (b : β a), γ a b

Dependent product of types is associative up to an equivalence.

Equations
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
@[simp]
theorem equiv.prod_congr_left_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) (b : β₁) (a : α₁) :
(b, a) = ((e a) b, a)
theorem equiv.prod_congr_refl_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ β₂) :
e.prod_congr (equiv.refl α₁) = equiv.prod_congr_left (λ (_x : α₁), e)
def equiv.prod_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
α₁ × β₁ α₁ × β₂

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

Equations
@[simp]
theorem equiv.prod_congr_right_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) (a : α₁) (b : β₁) :
(a, b) = (a, (e a) b)
theorem equiv.prod_congr_refl_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ β₂) :
(equiv.refl α₁).prod_congr e = equiv.prod_congr_right (λ (_x : α₁), e)
@[simp]
theorem equiv.prod_congr_left_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
α₁) = α₁).trans
@[simp]
theorem equiv.prod_congr_right_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
β₂) = β₁).trans
theorem equiv.sigma_congr_right_sigma_equiv_prod {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
β₂) = β₁).trans
theorem equiv.sigma_equiv_prod_sigma_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
β₁).symm.trans = β₂).symm
@[simp]
theorem equiv.of_fiber_equiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) (ᾰ : β) :
.symm) = ((.symm) (.symm) ᾰ)).snd)
@[simp]
theorem equiv.of_fiber_equiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) (ᾰ : α) :
= ((e (f ᾰ)) (.symm) ᾰ).snd)
def equiv.of_fiber_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) :
α β

A family of equivalences between fibers gives an equivalence between domains.

Equations
theorem equiv.of_fiber_equiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} (e : Π (c : γ), {a // f a = c} {b // g b = c}) (a : α) :
g a) = f a
@[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)
@[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)
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
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
@[simp]
theorem equiv.perm.prod_extend_right_apply_eq {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (b : β₁) :
(a, b) = (a, e b)
theorem equiv.perm.prod_extend_right_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (e : equiv.perm β₁) {a a' : α₁} (h : a' a) (b : β₁) :
(a', b) = (a', b)
theorem equiv.perm.eq_of_prod_extend_right_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] {e : equiv.perm β₁} {a a' : α₁} {b : β₁} (h : (a', b) (a', b)) :
a' = a
@[simp]
theorem equiv.perm.fst_prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (ab : α₁ × β₁) :
ab).fst = ab.fst
def equiv.arrow_prod_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(γ → α × β) (γ → α) × (γ → β)

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

Equations
def equiv.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
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β → γ) (a : α) :
( f).fst a = f (sum.inl a)
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_apply_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β → γ) (b : β) :
( f).snd b = f (sum.inr b)
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) (a : α) :
γ).symm) (f, g) (sum.inl a) = f a
@[simp]
theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) (b : β) :
γ).symm) (f, g) (sum.inr b) = g b
def equiv.sum_prod_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β) × γ α × γ β × γ

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

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

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

Equations
@[simp]
theorem equiv.prod_sum_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (b : β) :
γ) (a, sum.inl b) = sum.inl (a, b)
@[simp]
theorem equiv.prod_sum_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
γ) (a, sum.inr c) = sum.inr (a, c)
@[simp]
theorem equiv.sigma_sum_distrib_apply {ι : Type u_1} (α : ι → Type u_2) (β : ι → Type u_3) (p : Σ (i : ι), α i β i) :
p = sum.cases_on p.snd (λ (x : α p.fst), sum.inl p.fst, x⟩) (λ (x : β p.fst), sum.inr p.fst, x⟩)
def equiv.sigma_sum_distrib {ι : Type u_1} (α : ι → Type u_2) (β : ι → Type u_3) :
(Σ (i : ι), α i β i) (Σ (i : ι), α i) Σ (i : ι), β i

An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums.

Equations
@[simp]
theorem equiv.sigma_sum_distrib_symm_apply {ι : Type u_1} (α : ι → Type u_2) (β : ι → Type u_3) (ᾰ : (Σ (i : ι), α i) Σ (i : ι), β i) :
β).symm) = sum.elim (λ (_x : ι), sum.inl)) (λ (_x : ι), sum.inr))
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
def equiv.sigma_nat_succ (f : Type u) :
(Σ (n : ), f n) f 0 Σ (n : ), f (n + 1)

An equivalence that separates out the 0th fiber of `(Σ (n : ℕ), f n)`.

Equations
def equiv.bool_prod_equiv_sum (α : Type u) :
α α

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

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

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

Equations
@[simp]
theorem equiv.bool_arrow_equiv_prod_apply (α : Type u) (f : bool → α) :
= (f bool.tt, f bool.ff)
@[simp]
theorem equiv.bool_arrow_equiv_prod_symm_apply (α : Type u) (p : α × α) (b : bool) :
p b = cond b p.fst p.snd

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 : , 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 =
• equiv.nat_equiv_nat_sum_punit._match_1 0 =
• equiv.nat_equiv_nat_sum_punit._match_2 = 0
• equiv.nat_equiv_nat_sum_punit._match_2 (sum.inl n) = n.succ

`ℕ ⊕ punit` is equivalent to `ℕ`.

Equations

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

Equations
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
def equiv.unique_congr {α : Sort u} {β : Sort v} (e : α β) :

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

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

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

@[protected]
theorem equiv.is_empty {α : Sort u} {β : Sort v} (e : α β) [is_empty β] :
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
@[simp]
theorem equiv.subtype_equiv_refl {α : Sort u} {p : α → Prop} (h : (∀ (a : α), p a p ((equiv.refl α) a)) := _) :
h = equiv.refl {a // p a}
@[simp]
theorem equiv.subtype_equiv_symm {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) (h : ∀ (a : α), p a q (e a)) :
@[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)) :
@[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, _⟩
@[simp]
theorem equiv.subtype_equiv_right_symm_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x q x) (b : {b // (λ (x : α), q x) b}) :
( b) = b
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
@[simp]
theorem equiv.subtype_equiv_right_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x q x) (a : {a // (λ (x : α), p x) a}) :
a) = a
def equiv.subtype_equiv_of_subtype {α : Sort u} {β : Sort v} {p : β → Prop} (e : α β) :
{a // p (e a)} {b // p b}

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

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

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

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

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

Equations
def equiv.subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : → Prop) :
{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
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_exists_symm_apply_coe_coe {α : Type u} (p : α → Prop) (q : → Prop) (a : {a // ∃ (h : p a), q a, h⟩}) :
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_exists_apply_coe {α : Type u} (p : α → Prop) (q : → Prop) (a : subtype q) :
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
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_inter_apply_coe {α : Type u} (p q : α → Prop) (ᾰ : {x // q x.val}) :
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_inter_symm_apply_coe_coe {α : Type u} (p q : α → Prop) (ᾰ : {x // p x q x}) :
ᾰ) =
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_symm_apply_coe_coe {α : Type u} {p q : α → Prop} (h : ∀ {x : α}, q xp x) (ᾰ : subtype q) :
ᾰ) =
@[simp]
theorem equiv.subtype_subtype_equiv_subtype_apply_coe {α : Type u} {p q : α → Prop} (h : ∀ {x : α}, q xp x) (ᾰ : {x // q x.val}) :
def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x : α}, q xp x) :
{x // q x.val}

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

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

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

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

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

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

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

Equations
def equiv.sigma_subtype_fiber_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
def equiv.sigma_subtype_fiber_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})

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations
@[simp]
theorem equiv.coe_subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) :
= λ (g : {g // g coe = f}), g x
@[simp]
theorem equiv.subtype_equiv_codomain_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (g : {g // g coe = f}) :
= g x
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) :
= λ (y : Y), λ (x' : X), dite (x' x) (λ (h : x' x), f x', h⟩) (λ (h : ¬x' x), y), _⟩
@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (y : Y) (x' : X) :
y) x' = dite (x' x) (λ (h : x' x), f x', h⟩) (λ (h : ¬x' x), y)
@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply_eq {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (y : Y) :
y) x = y
theorem equiv.subtype_equiv_codomain_symm_apply_ne {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (y : Y) (x' : X) (h : x' x) :
y) x' = f x', h⟩
noncomputable def equiv.of_bijective {α : Sort u} {β : Sort v} (f : α → β) (hf : function.bijective f) :
α β

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

Equations
@[simp]
theorem equiv.of_bijective_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : function.bijective f) (ᾰ : α) :
hf) = f ᾰ
theorem equiv.of_bijective_apply_symm_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : function.bijective f) (x : β) :
f ( hf).symm) x) = x
@[simp]
theorem equiv.of_bijective_symm_apply_apply {α : Sort u} {β : Sort v} (f : α → β) (hf : function.bijective f) (x : α) :
hf).symm) (f x) = x
@[protected, instance]
def equiv.can_lift {α : Sort u} {β : Sort v} :
can_lift (α → β) β)
Equations
def equiv.perm.extend_domain {α' : Type u_1} {β' : Type u_2} (e : equiv.perm α') {p : β' → Prop} (f : α' ) :

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.o`