stoppedValue_piecewise_const — Mathlib

English

If f is a function and S is a set, then the stoppedValue of a piecewise constant function equals the piecewise combination of the stopped values at the two constants.

Русский

Если f — функция, а S — множество, то stoppedValue для кусочно константной функции равен кусочно-константному сочетанию значений остановленных величин.

LaTeX

$$$\text{stoppedValue } f (s.piecewise (\text{const } i) (\text{const } j)) = s.piecewise (f i) (f j)$$$

Lean4

theorem stoppedValue_piecewise_const {ι' : Type*} {i j : ι'} {f : ι' → Ω → ℝ} :
    stoppedValue f (s.piecewise (fun _ => i) fun _ => j) = s.piecewise (f i) (f j) := by ext ω; rw [stoppedValue];
  by_cases hx : ω ∈ s <;> simp [hx]

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