isOpenPosMeasure

Mathlib.MeasureTheory.Measure.OpenPos

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

English

If μ ≪ ν, then ν is open-positive.

Русский

Если μ абсолютно непрерывна относительно ν, то ν открыто положительна.

LaTeX

$$$\mu \ll \nu \Rightarrow \text{IsOpenPosMeasure}(\nu).$$$

Lean4

protected theorem isOpenPosMeasure (h : μ ≪ ν) : IsOpenPosMeasure ν :=
  ⟨fun _U ho hne h₀ => ho.measure_ne_zero μ hne (h h₀)⟩

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

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

Разделы

Аффилиация

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