sSup — Mathlib

English

If a set of functions is all ωScottContinuous, then their pointwise sSup is ωScottContinuous.

Русский

Если множество функций ωScott непрерывных, то их покомпонентный суп сохраняет ωScott непрерывность.

LaTeX

$$$\forall s, (\forall f \in s, ωScottContinuous f) \Rightarrow ωScottContinuous (sSup s)$$

Lean4

theorem sSup {s : Set (α → β)} (hs : ∀ f ∈ s, ωScottContinuous f) : ωScottContinuous (sSup s) := by rw [sSup_eq_iSup];
  exact ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f

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