piecewise_apply

Mathlib.Probability.Kernel.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.piecewise_apply

English

For any a, piecewise hs κ η acting on a gives κ(a) if a ∈ s and η(a) otherwise.

Русский

Для любого a применение piecewise к a дает κ(a), если a ∈ s, иначе η(a).

LaTeX

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

Lean4

theorem piecewise_apply (a : α) : piecewise hs κ η a = if a ∈ s then κ a else η a :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru