ciSup_eq_monotonicSequenceLimit — Mathlib

English

For ConditionallyCompleteLattice α and WellFoundedGT α, iSup a = monotonicSequenceLimit a for a monotone sequence a.

Русский

Для частично полноупорядоченного множества α и WellFoundedGT α, iSup a совпадает с monotonicSequenceLimit a для монотонной последовательности a.

LaTeX

$$$$\mathrm{iSup}\; a = \mathrm{monotonicSequenceLimit}(a).$$$$

Lean4

theorem ciSup_eq_monotonicSequenceLimit [ConditionallyCompleteLattice α] [WellFoundedGT α] (a : ℕ →o α)
    (ha : BddAbove (Set.range a)) : iSup a = monotonicSequenceLimit a :=
  (ciSup_le (le_monotonicSequenceLimit a)).antisymm (le_ciSup ha _)

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