invariants_le — Mathlib

English

The invariant σ-algebra of f is contained in the ambient measurable σ-algebra: every f-invariant set is measurable.

Русский

Инвариантная σ-алгебра по f содержится в заданной измеримой σ-алгебре: каждое f-инвариантное множество измеримо.

LaTeX

$$$ invariants(f) \\\\le \\\\mathcal{M}$$$

Lean4

theorem invariants_le (f : α → α) : invariants f ≤ ‹MeasurableSpace α› := fun _ ↦ And.left

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