neBot

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

If μ is nonzero, then (ae μ).NeBot holds as an instance.

Русский

Если μ не ноль, тогда (ae μ).NeBot существует как экземпляр.

LaTeX

$$instance ae_neBot [NeZero μ] : (ae μ).NeBot$$

Lean4

instance neBot [NeZero μ] : (ae μ).NeBot :=
  ae_neBot.2 <| NeZero.ne μ

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

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

Разделы

Аффилиация

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