ωSup_eq_of_isLUB — Mathlib

English

If Set.range(c) is an IsLUB element a, then a = ωSup c.

Русский

Если для цепи c множество значений является IsLUB с верхней гранью a, то a равно ωSup c.

LaTeX

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

Lean4

theorem ωSup_eq_of_isLUB {c : Chain α} {a : α} (h : IsLUB (Set.range c) a) : a = ωSup c :=
  by
  rw [le_antisymm_iff]
  simp only [IsLUB, IsLeast, upperBounds, lowerBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
    Set.mem_setOf_eq] at h
  constructor
  · apply h.2
    exact fun a ↦ le_ωSup c a
  · rw [ωSup_le_iff]
    apply h.1

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