iterate_lt — Mathlib

English

If a < o and o is principal, then for all n, (op a)^[n] a < o.

Русский

Если a < o и o — principal, то для всех n выполняется (op a)^[n] a < o.

LaTeX

$$$$ \forall a,o,\ \operatorname{partialOrder}.\lt a o \wedge \operatorname{Principal}(op)\ o \Rightarrow \forall n:\mathbb{N},\ \operatorname{partialOrder}.lt( (op\ a)^[n]\ a)\ o. $$$$

Lean4

theorem iterate_lt (hao : a < o) (ho : Principal op o) (n : ℕ) : (op a)^[n] a < o := by
  induction n with
  | zero => rwa [Function.iterate_zero]
  | succ n hn =>
    rw [Function.iterate_succ']
    exact ho hao hn

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