Commit 2022-10-27 07:38 9340cc93

feat(data/nat/interval): Cauchy induction (#15880) This PR shows that if a predicate on the natural numbers is downward closed, i.e. satisfying ∀ n, P (n + 1) → P n, then in order for it to hold for all natural numbers, it suffices that it holds for a set of natural numbers satisfying the following three equivalent conditions: (1) unbounded (¬ bdd_above), (2) infinite, and (3) nonempty without a maximal element. The last version (nonempty + no-max) is the essence of Cauchy induction (cauchy_induction'): nonemptiness is stated in this PR as a "seed" such that P seed holds, and the no-max condition is stated as ∀ x, seed ≤ x → P x → ∃ y, x < y ∧ P y. When we have P x → P (k * x) for some k > 1, we may take y := k * x, which satisfies x < y when x > 0, so we just need to take seed ≥ 1; this is the classical, more restricted version of Cauchy induction (cauchy_induction_mul).