isOpenPosMeasure_smul

Mathlib.MeasureTheory.Measure.OpenPos

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.isOpenPosMeasure_smul

English

For any c ≠ 0, c • μ is open-positive if μ is open-positive.

Русский

При любом c ≠ 0, если μ открыто положительна, то c•μ так же открыто положительна.

LaTeX

$$$c \neq 0 \Rightarrow \text{IsOpenPosMeasure}(c\cdot μ).$$$

Lean4

theorem isOpenPosMeasure_smul {c : ℝ≥0∞} (h : c ≠ 0) : IsOpenPosMeasure (c • μ) :=
  ⟨fun _U Uo Une => mul_ne_zero h (Uo.measure_ne_zero μ Une)⟩

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

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

Разделы

Аффилиация

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