pos_mono

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

If μ ≪ ν and μ is positive on a set t (i.e., μ(t) > 0), then ν(t) > 0 as well.

Русский

Если μ ≪ ν и μ(t) > 0, то ν(t) > 0.

LaTeX

$$∀ t, 0 < μ(t) → 0 < ν(t)$$

Lean4

theorem pos_mono {μ ν : Measure α} (hμν : μ ≪ ν) ⦃t : Set α⦄ (ht : 0 < μ t) : 0 < ν t :=
  by
  contrapose! ht
  simp_all [hμν.null_mono]

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

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

Разделы

Аффилиация

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