isLUB — Mathlib

English

If f is ωScott-continuous, then f is monotone.

Русский

Если f ωScott-непрерывна, то она монотонна.

LaTeX

$$$$ \text{ωScottContinuous } f \Rightarrow \text{Monotone } f. $$$$

Lean4

theorem isLUB {c : Chain α} (hf : ωScottContinuous f) : IsLUB (Set.range (c.map ⟨f, hf.monotone⟩)) (f (ωSup c)) := by
  simpa [map_coe, OrderHom.coe_mk, Set.range_comp] using
    hf (by simp) (Set.range_nonempty _) (isChain_range c).directedOn (isLUB_range_ωSup c)

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