piecewise_compl — Mathlib

English

If s^c is measurable, then piecewise on s^c with hs is equal to piecewise on s with f and g swapped.

Русский

Если s^c измеримо, то piecewise на s^c с hs равен piecewise на s с поменянными местами f и g.

LaTeX

$$$$ \\text{piecewise}(s^{c},\\, hs,\\ f,\\ g) = \\text{piecewise}(s,\\, hs.of\\_compl,\\ g,\\ f). $$$$

Lean4

@[simp]
theorem piecewise_compl {s : Set α} (hs : MeasurableSet sᶜ) (f g : α →ₛ β) :
    piecewise sᶜ hs f g = piecewise s hs.of_compl g f :=
  coe_injective <| by simp

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