isLUB_range_ωSup — Mathlib

English

For any chain c, the range of c is a set whose least upper bound is ωSup c.

Русский

Для любой цепи c множество его значений имеет наименьшую верхнюю грань равную ωSup c.

LaTeX

$$$$ \text{IsLUB}(\operatorname{Set.range} c, \omegaSup c). $$$$

Lean4

theorem isLUB_range_ωSup (c : Chain α) : IsLUB (Set.range c) (ωSup c) :=
  by
  constructor
  · simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff, Set.mem_setOf_eq]
    exact fun a ↦ le_ωSup c a
  · simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff, Set.mem_setOf_eq]
    exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

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