measurableSet_graph — Mathlib

English

Let f: α → ℝ be a measurable function. Then its graph, viewed as a subset of α × ℝ, is measurable.

Русский

Пусть f: α → ℝ измерима. График f, рассматриваемый как подмножество α × ℝ, измерим.

LaTeX

$$$\text{MeasurableSet}\{(x,y) \in \alpha \times \mathbb{R} \mid y = f(x)\}$$$

Lean4

/-- The graph of a measurable function is a measurable set. -/
theorem measurableSet_graph (hf : Measurable f) : MeasurableSet {p : α × ℝ | p.snd = f p.fst} := by
  simpa using measurableSet_region_between_cc hf hf MeasurableSet.univ

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