le_invariants_iterate — Mathlib

English

For any f : α → α and natural n, the invariant σ-algebra of f is contained in the invariant σ-algebra of the n-th iterate f^[n].

Русский

Для любой f: α → α и натурального n, инвариантная σ-алгебра f содержится в инвариантной σ-алгебре f^[n].

LaTeX

$$$\\\\operatorname{invariants}(f) \\\\le \\\\operatorname{invariants}(f^{[n]})$$

Lean4

theorem le_invariants_iterate (f : α → α) (n : ℕ) : invariants f ≤ invariants (f^[n]) := by
  induction n with
  | zero => simp [invariants_le]
  | succ n ihn => exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

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