English
Let p be a predicate on α and f a function ∀ a, p a → β. The domain of the partial function x ↦ ⟨p x, f x⟩ is exactly {x | p x}.
Русский
Пусть p: α → Prop, f: ∀ a, p a → β. Область частичной функции x ↦ ⟨p x, f x⟩ равна множеству {x | p x}.
LaTeX
$$$\\mathrm{Dom}(\\lambda x. \\langle p(x), f(x)\\rangle) = \\{ x \\mid p(x) \\}$$$
Lean4
@[simp]
theorem dom_mk (p : α → Prop) (f : ∀ a, p a → β) : (PFun.Dom fun x => ⟨p x, f x⟩) = {x | p x} :=
rfl