piecewise_univ

Mathlib.MeasureTheory.Function.SimpleFunc

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

English

If we take the entire space as the domain, piecewise univ reduces to f.

Русский

Если область определения — всё пространство, то piecewise на univ сводится к f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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