iSup — Mathlib

English

If f i are ωScottContinuous (i ranging over an index set), then the function i ↦ ⨆ i f i is ωScottContinuous.

Русский

Если для каждого i функция f i ωScott непрерывна, то функция i ↦ ⨆ i f i непрерывна в смысле ωScott.

LaTeX

$$$\forall i, ωScottContinuous (f i) \Rightarrow ωScottContinuous (iSup i \; f i)$$$

Lean4

theorem iSup {f : ι → α → β} (hf : ∀ i, ωScottContinuous (f i)) : ωScottContinuous (⨆ i, f i) :=
  by
  refine
    ωScottContinuous.of_monotone_map_ωSup
      ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
  simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_swap ι]

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