asSubtype — Mathlib

English

Turns a partial function into a genuine function defined on its domain: for s ∈ Dom f, asSubtype(f)(s) = f(s) where s is a pair ⟨a, ha⟩ with ha: a ∈ Dom f.

Русский

Превращает частичную функцию в обычную функцию, определённую на области определения: для s = ⟨a, ha⟩ из f.Dom выполняется asSubtype(f)(s) = f(a)(ha).

LaTeX

$$$\\text{asSubtype}(f)(\\langle x, dx \\rangle) = f(x)(dx)$$$

Lean4

/-- Turns a partial function into a function out of its domain. -/
def asSubtype (f : α →. β) (s : f.Dom) : β :=
  f.fn s s.2

Похожие утверждения