range_indicator — Mathlib

English

If s is measurable, nonempty, and not universal, then the range of the two-valued piecewise function equals {x, y}.

Русский

Пусть s измеримо, непусто и не равно всему пространству; диапазон функции piecewise имеет два значения x и y.

LaTeX

$$$$ \\mathrm{range}\\big(\\text{piecewise}(s, hs, \\mathbf{const}(x), \\mathbf{const}(y))) = \\{x, y\\}. $$$$

Lean4

theorem range_indicator {s : Set α} (hs : MeasurableSet s) (hs_nonempty : s.Nonempty) (hs_ne_univ : s ≠ univ)
    (x y : β) : (piecewise s hs (const α x) (const α y)).range = { x, y } := by
  simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const, Finset.coe_insert,
    Finset.coe_singleton, hs_nonempty.image_const, (nonempty_compl.2 hs_ne_univ).image_const, singleton_union,
    Function.const]

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