piecewise_apply — Mathlib

English

For any a, the value of piecewise s hs f g at a equals f a if a ∈ s, and g a otherwise.

Русский

Для любого a значение piecewise s hs f g в точке a равно f(a), если a ∈ s, иначе g(a).

LaTeX

$$$$ (\\text{piecewise } s\\ hs\\ f\\ g)(a) = \\begin{cases} f(a), & a \\in s \\\\ g(a), & a \\notin s \\end{cases} $$$$

Lean4

theorem piecewise_apply {s : Set α} (hs : MeasurableSet s) (f g : α →ₛ β) (a) :
    piecewise s hs f g a = if a ∈ s then f a else g a :=
  rfl

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