tilted_zero_measure

Mathlib.MeasureTheory.Measure.Tilted

URI: https://scilib.ai/kg/mathlib#MeasureTheory.tilted_zero_measure

English

For any function f, the tilted measure of the zero measure is zero.

Русский

Для любой функции f тильдированная мера нулевой меры равна нулю.

LaTeX

$$$\\text{tilted}(0) = 0$$$

Lean4

@[simp]
theorem tilted_zero_measure (f : α → ℝ) : (0 : Measure α).tilted f = 0 := by simp [Measure.tilted]

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

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

Разделы

Аффилиация

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