mathlib documentation

core.init.funext

def function.equiv {α : Sort u} {β : α → Sort v} :
(Π (x : α), β x)(Π (x : α), β x) → Prop

Equations
theorem function.equiv.refl {α : Sort u} {β : α → Sort v} (f : Π (x : α), β x) :

theorem function.equiv.symm {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x} :
function.equiv f₁ f₂function.equiv f₂ f₁

theorem function.equiv.trans {α : Sort u} {β : α → Sort v} {f₁ f₂ f₃ : Π (x : α), β x} :
function.equiv f₁ f₂function.equiv f₂ f₃function.equiv f₁ f₃

theorem function.equiv.is_equivalence (α : Sort u) (β : α → Sort v) :

@[ext]
theorem funext {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x} :
(∀ (x : α), f₁ x = f₂ x)f₁ = f₂

@[instance]
def pi.subsingleton {α : Sort u} {β : α → Sort v} [∀ (a : α), subsingleton (β a)] :
subsingleton (Π (a : α), β a)