dom_mk — Mathlib

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

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