core / init.funext - mathlib docs

source

@[protected]

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

Prop

The relation stating that two functions are pointwise equal.

Equations

function.equiv f₁ f₂ = ∀ (x : α), f₁ x = f₂ x

source

@[protected]

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

function.equiv f f

source

@[protected]

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

function.equiv f₁ f₂ → function.equiv f₂ f₁

source

@[protected]

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₃

source

@[protected]

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

equivalence function.equiv

source

def function.fun_setoid (α : Sort u) (β : α → Sort v) :

setoid (Π (x : α), β x)

The setoid generated by pointwise equality.

Equations

function.fun_setoid α β = {r := function.equiv β, iseqv := _}

source

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

Sort (imax u v)

The quotient of the function type by pointwise equality.

Equations

function.extfun α β = quotient (function.fun_setoid α β)

source

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

function.extfun α β

The map from functions into the qquotient by pointwise equality.

Equations

function.fun_to_extfun f = ⟦f⟧

source

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

β x

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

Equations

function.extfun_app f = λ (x : α), quot.lift_on f (λ (f : Π (x : α), β x), f x) _

source

@[ext]

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

f₁ = f₂

Function extensionality, proven using quotients.

source

@[protected, instance]

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

subsingleton (Π (a : α), β a)