dom_eq

Mathlib.Data.PFun

URI: https://scilib.ai/kg/mathlib#PFun.dom_eq

English

For any partial function f, the domain of f is exactly the set {x | ∃ y, y ∈ f(x)}.

Русский

Для любой частичной функции f область определения равна множеству {x | ∃ y, y ∈ f(x)}.

LaTeX

$$$\\mathrm{Dom}(f) = \\{ x \\mid \\exists y, y \\in f(x) \\}$$$

Lean4

theorem dom_eq (f : α →. β) : Dom f = {x | ∃ y, y ∈ f x} :=
  Set.ext (mem_dom f)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru