mathlibdocumentation

core / init.funext

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

The relation stating that two functions are pointwise equal.

Equations
• f₂ = ∀ (x : α), f₁ x = f₂ x
@[protected]
theorem function.equiv.refl {α : Sort u} {β : α → Sort v} (f : Π (x : α), β x) :
@[protected]
theorem function.equiv.symm {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x} :
f₂ f₁
@[protected]
theorem function.equiv.trans {α : Sort u} {β : α → Sort v} {f₁ f₂ f₃ : Π (x : α), β x} :
f₂ f₃ f₃
@[protected]
theorem function.equiv.is_equivalence (α : Sort u) (β : α → Sort v) :
def function.fun_setoid (α : Sort u) (β : α → Sort v) :
setoid (Π (x : α), β x)

The setoid generated by pointwise equality.

Equations
def function.extfun (α : Sort u) (β : α → Sort v) :
Sort (imax u v)

The quotient of the function type by pointwise equality.

Equations
def function.fun_to_extfun {α : Sort u} {β : α → Sort v} (f : Π (x : α), β x) :

The map from functions into the qquotient by pointwise equality.

Equations
def function.extfun_app {α : Sort u} {β : α → Sort v} (f : β) (x : α) :
β x

From an element of extfun we can retrieve an actual function.

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

Function extensionality, proven using quotients.

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