ae_neBot

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ae_neBot

English

(ae μ).NeBot iff μ ≠ 0.

Русский

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

LaTeX

$$(ae μ).NeBot \iff μ \neq 0$$

Lean4

@[simp]
theorem ae_neBot : (ae μ).NeBot ↔ μ ≠ 0 :=
  neBot_iff.trans (not_congr ae_eq_bot)

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

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

Разделы

Аффилиация

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