piecewise_empty

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.piecewise_empty

English

If s is empty, the piecewise function equals g.

Русский

Если s пусто, получаемое piecewise равно g.

LaTeX

$$$$ \\text{piecewise}(\\emptyset, \\mathrm{MeasurableSet.empty}, f, g) = g $$$$

Lean4

@[simp]
theorem piecewise_empty (f g : α →ₛ β) : piecewise ∅ MeasurableSet.empty f g = g :=
  coe_injective <| by simp

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

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

Разделы

Аффилиация

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