isωSup_iff_isLUB — Mathlib

English

IsωSup c x is equivalent to IsLUB (range c) x; i.e., x is the least upper bound of the range of c.

Русский

IsωSup c x эквивалентно IsLUB (range c) x; то есть x — наименьшее верхнее предел диапазона c.

LaTeX

$$$IsωSup(c, x) \iff IsLUB(\operatorname{range}(c), x).$$$

Lean4

theorem isωSup_iff_isLUB {α : Type u} [Preorder α] {c : Chain α} {x : α} : IsωSup c x ↔ IsLUB (range c) x := by
  simp [IsωSup, IsLUB, IsLeast, upperBounds, lowerBounds]

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