dite — Mathlib

English

A measurable function defined by cases on x ∈ s or not is measurable.

Русский

Измеримая функция, заданная по веткам x ∈ s и x ∉ s, измерима.

LaTeX

$$$\\\\operatorname{Measurable}(\\\\dite)$$$$

Lean4

theorem dite [∀ x, Decidable (x ∈ s)] {f : s → β} (hf : Measurable f) {g : (sᶜ : Set α) → β} (hg : Measurable g)
    (hs : MeasurableSet s) : Measurable fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩ :=
  measurable_of_restrict_of_restrict_compl hs (by simpa) (by simpa)

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