zero_measure

Mathlib.Dynamics.Ergodic.Ergodic

URI: https://scilib.ai/kg/mathlib#Ergodic.zero_measure

← MathLib Explorer

English

The zero measure is ergodic for any measurable f.

Русский

Нулевая мера эргодична для любого измеримого отображения f.

LaTeX

$$$\mathrm{Ergodic}(f, 0)$$$

Lean4

theorem zero_measure {f : α → α} (hf : Measurable f) : @Ergodic α m f 0
    where
  measurable := hf
  map_eq := by simp
  toPreErgodic := .zero_measure f

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

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

Разделы

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

Аффилиация

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