exists_pred_iterate_or — Mathlib

English

In a linear order with IsPredArchimedean, for any a,b there exists n such that pred^[n](b) = a or pred^[n](a) = b.

Русский

При preds-архимедовости: существует n такое, что pred^[n](b) = a или pred^[n](a) = b.

LaTeX

$$$ \forall a,b,\ (\exists n, \mathrm{iterate\_pred}(n,b)=a) \lor (\exists n, \mathrm{iterate\_pred}(n,a)=b).$$$

Lean4

theorem exists_pred_iterate_or : (∃ n, pred^[n] b = a) ∨ ∃ n, pred^[n] a = b :=
  (le_total a b).imp exists_pred_iterate_of_le exists_pred_iterate_of_le

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