ae_notMem

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

URI: https://scilib.ai/kg/mathlib#Set.Countable.ae_notMem

← MathLib Explorer

English

For a countable s, μ-a.e. x is not in s.

Русский

Для счетного множества s μ-a.e. x не принадлежит s.

LaTeX

$$$$\forall^* x: x \notin s \text{ (ae μ)}.$$$$

Lean4

theorem _root_.Set.Countable.ae_notMem (h : s.Countable) (μ : Measure α) [NoAtoms μ] : ∀ᵐ x ∂μ, x ∉ s := by
  simpa only [ae_iff, Classical.not_not] using h.measure_zero μ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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