ωSupImpl — Mathlib

English

The supremum of a chain in the product ω-CPO is the pair of the supremums of the projections: ωSup (c) = (ωSup (fst ∘ c), ωSup (snd ∘ c)).

Русский

Найдём точку верхней грани для произведения ω-CPO: супремум цепи в произведении равен паре супремумов проекций.

LaTeX

$$$\omegaSup(c) = (\omegaSup(\mathrm{map\ fst}\ c), \omegaSup(\mathrm{map\ snd}\ c))$$$

Lean4

/-- The supremum of a chain in the product `ω`-CPO. -/
@[simps]
protected def ωSupImpl (c : Chain (α × β)) : α × β :=
  (ωSup (c.map OrderHom.fst), ωSup (c.map OrderHom.snd))

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