iterate_pos_lt_iff_map_lt' — Mathlib

English

Same equivalence as above but with the primed variant.

Русский

Та же эквивалентность для варианта с апострофом.

LaTeX

$$$\\text{Function.Commute}(f,g) \\Rightarrow \\forall x, \\forall n>0, (f^{[n]} x < g^{[n]} x) \\iff (f x < g x).$$$

Lean4

theorem iterate_pos_lt_iff_map_lt' (h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x n} (hn : 0 < n) :
    f^[n] x < g^[n] x ↔ f x < g x :=
  @iterate_pos_lt_iff_map_lt αᵒᵈ _ _ _ h.symm hg.dual hf.dual x n hn

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