piecewise_apply' — Mathlib

English

For any a and t, the measure satisfies piecewise hs κ η a t = κ a t if a ∈ s and = η a t otherwise.

Русский

Для любых a, t: piecewise hs κ η a t = κ a t если a ∈ s и = η a t иначе.

LaTeX

$$$\\text{piecewise}(s,\\kappa,\\eta)(a)(t) = \\begin{cases} \\kappa(a)(t) & a \\in s \\\\ \\eta(a)(t) & a \\notin s \\end{cases}$$$

Lean4

theorem piecewise_apply' (a : α) (t : Set β) : piecewise hs κ η a t = if a ∈ s then κ a t else η a t := by
  rw [piecewise_apply]; split_ifs <;> rfl

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