exists_succ_iterate_or — Mathlib

English

In a linear order with a succ-Archimedean property, for any a,b there exists n such that succ^[n](a) = b or succ^[n](b) = a.

Русский

В линейном порядке с свойством succ-архимедности существует такое число n, что succ^[n](a) = b или succ^[n](b) = a.

LaTeX

$$$ \forall a,b,\ (\exists n \in \mathbb{N}, \ succ^{[n]}(a) = b ) \lor (\exists n \in \mathbb{N}, \ succ^{[n]}(b) = a).$$$

Lean4

theorem exists_succ_iterate_or : (∃ n, succ^[n] a = b) ∨ ∃ n, succ^[n] b = a :=
  (le_total a b).imp exists_succ_iterate_of_le exists_succ_iterate_of_le

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