measure_const

Mathlib.MeasureTheory.Measure.Stieltjes

URI: https://scilib.ai/kg/mathlib#StieltjesFunction.measure_const

English

For any real constant c, the measure of the constant Stieltjes function is zero: (const c).measure = 0.

Русский

Для любой постоянной функции c мера константы равна нулю: (const c).measure = 0.

LaTeX

$$$(\\\\text{StieltjesFunction.const } c).\\\\mathrm{measure} = 0$$$

Lean4

@[simp]
theorem measure_const (c : ℝ) : (StieltjesFunction.const c).measure = 0 :=
  Measure.ext_of_Ioc _ _ (by simp)

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

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

Разделы

Аффилиация

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