Ioi_ae_eq_Ici'

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Ioi_ae_eq_Ici'

English

(ae μ).NeBot is equivalent to μ ≠ 0

Русский

NeBot(ae μ) эквивалентно μ ≠ 0.

LaTeX

$$(ae μ).NeBot ↔ μ ≠ 0$$

Lean4

theorem Ioi_ae_eq_Ici' (ha : μ { a } = 0) : Ioi a =ᵐ[μ] Ici a :=
  Iio_ae_eq_Iic' (α := αᵒᵈ) ha

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

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

Разделы

Аффилиация

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