iSup_eq_monotonicSequenceLimit — Mathlib

English

Same as above: for all m, a(m) ≤ monotonicSequenceLimit a under the same assumptions.

Русский

То же самое: для любого m выполняется a(m) ≤ monotonicSequenceLimit a при тех же предпосылках.

LaTeX

$$$$\forall m,\ a(m) \le \mathrm{monotonicSequenceLimit}(a).$$$$

Lean4

theorem iSup_eq_monotonicSequenceLimit [CompleteLattice α] [WellFoundedGT α] (a : ℕ →o α) :
    iSup a = monotonicSequenceLimit a :=
  (iSup_le (le_monotonicSequenceLimit a)).antisymm (le_iSup a _)

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