IsωSup — Mathlib

English

For any chain c, IsωSup c (ωSup c) holds; i.e., the ω-sup of a chain is a least upper bound of its range.

Русский

Для любой цепи c выполнено IsωSup c (ωSup c); ω-предельная сумма цепи является наименьшим верхним пределом ее диапазона.

LaTeX

$$$\text{IsωSup}(c, \omegaSup(c)).$$$

Lean4

/-- `x` is an `ω`-Sup of a chain `c` if it is the least upper bound of the range of `c`. -/
def IsωSup {α : Type u} [Preorder α] (c : Chain α) (x : α) : Prop :=
  (∀ i, c i ≤ x) ∧ ∀ y, (∀ i, c i ≤ y) → x ≤ y

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