ωSup — Mathlib

English

If some a belongs to a Chain of Part α, then ωSup equals some a.

Русский

Если some a принадлежит цепи Part α, то ωSup равен some a.

LaTeX

$$$$ \forall c: \text{Chain }(\text{Part }\alpha), \ \text{if } \text{some } a \in c, \text{ then } Part.\omegaSup c = Part.some a. $$$$

Lean4

/-- The (noncomputable) `ωSup` definition for the `ω`-CPO structure on `Part α`. -/
protected noncomputable def ωSup (c : Chain (Part α)) : Part α :=
  if h : ∃ a, some a ∈ c then some (Classical.choose h) else none

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