mathlib documentation

core.init.funext

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

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

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

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

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

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

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