piecewise — Mathlib

English

Given a measurable set s and simple functions f and g, define a new simple function that equals f on s and g on the complement of s.

Русский

Задано измеримое множество s и простые функции f и g. Определим новую простую функцию, которая равна f на s и равна g на дополнении s.

LaTeX

$$$$ \\text{piecewise}(s, hs, f, g) \\;: \\; \\alpha \\to_\\mathrm{SimpleFunc} \\beta \\quad \\text{is the function that equals } f \\text{ on } s \\text{ and } g \\text{ on } s^c. $$$$

Lean4

/-- If-then-else as a `SimpleFunc`. -/
def piecewise (s : Set α) (hs : MeasurableSet s) (f g : α →ₛ β) : α →ₛ β :=
  ⟨s.piecewise f g, fun _ =>
    letI : MeasurableSpace β := ⊤
    f.measurable.piecewise hs g.measurable trivial,
    (f.finite_range.union g.finite_range).subset range_ite_subset⟩

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