mem_dom — Mathlib

English

For every partial function f: α →. β and every x ∈ α, x is in the domain of f if and only if there exists a y with y ∈ f(x).

Русский

Для любой частичной функции f: α →. β и любого x ∈ α верно: x принадлежит области определения f тогда и только тогда, когда существует элемент y, такой что y ∈ f(x).

LaTeX

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

Lean4

@[simp]
theorem mem_dom (f : α →. β) (x : α) : x ∈ Dom f ↔ ∃ y, y ∈ f x := by simp [Dom, Part.dom_iff_mem]

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