measure_self_or_compl_eq_zero

Mathlib.Dynamics.Ergodic.Ergodic

URI: https://scilib.ai/kg/mathlib#PreErgodic.measure_self_or_compl_eq_zero

← MathLib Explorer

English

For a PreErgodic f, measurable s with invariance, μ(s)=0 or μ(s^c)=0.

Русский

Для PreErgodic f, измеримого s c инвариантность, μ(s)=0 или μ(s^c)=0.

LaTeX

$$$\mu(s)=0 \lor \mu(s^{c})=0$.$$

Lean4

theorem measure_self_or_compl_eq_zero (hf : PreErgodic f μ) (hs : MeasurableSet s) (hs' : f ⁻¹' s = s) :
    μ s = 0 ∨ μ sᶜ = 0 := by simpa using hf.ae_empty_or_univ hs hs'

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

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

Разделы

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

Аффилиация

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