charFun_zero_measure

Mathlib.MeasureTheory.Measure.CharacteristicFunction

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

English

For the zero measure μ = 0 on E, we have χ_μ(t) = 0 for every t.

Русский

Для нулевой меры μ = 0 на E выполняется χ_μ(t) = 0 для всех t.

LaTeX

$$$$\\chi_{0}(t) = 0.$$$$

Lean4

@[simp]
theorem charFun_zero_measure : charFun (0 : Measure E) t = 0 := by simp [charFun_apply]

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

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

Разделы

Аффилиация

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