iterate_mono — Mathlib

English

If f ≤ g in CircleDeg1Lift, then for every natural n, the n-th iterate preserves the order: f^[n] ≤ g^[n].

Русский

Если f ≤ g в CircleDeg1Lift, то для каждого натурального n н-й итерат сохраняет порядок: f^[n] ≤ g^[n].

LaTeX

$$$ \forall {f,g : CircleDeg1Lift}, \; f \le g \Rightarrow \forall n \in \mathbb{N}, \; f^{[n]} \le g^{[n]}. $$$

Lean4

theorem iterate_mono {f g : CircleDeg1Lift} (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n] :=
  iterate_monotone n h

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