mathlib documentation

core / init.funext

def function.equiv {α : Sort u} {β : α → Sort v} (f₁ f₂ : Π (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} (h : ∀ (x : α), f₁ x = f₂ x) :
f₁ = f₂
def pi.subsingleton {α : Sort u} {β : α → Sort v} [∀ (a : α), subsingleton (β a)] :
subsingleton (Π (a : α), β a)