dom_iff_graph — Mathlib

English

An input x belongs to the domain of f if and only if there exists y with (x,y) in the graph of f.

Русский

Пусть x принадлежит области определения f тогда и только тогда, когда существует y such that (x,y) принадлежит графу f.

LaTeX

$$$x \\in \\mathrm{Dom}(f) \\iff \\exists y, (x,y) \\in \\mathrm{graph}(f)$$$

Lean4

theorem dom_iff_graph (f : α →. β) (x : α) : x ∈ f.Dom ↔ ∃ y, (x, y) ∈ f.graph :=
  Part.dom_iff_mem

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