isOpen_sUnion — Mathlib

English

The union of any (finite or infinite) collection of Scott-open sets is Scott-open.

Русский

Объединение любой (конечной или бесконечной) коллекции Scott-открытых множеств открыто.

LaTeX

$$$\forall \mathcal{S} \subseteq \mathcal{P}(X), \ \forall s_i \in \mathcal{S}, IsOpen(s_i) \Rightarrow IsOpen(\bigcup \mathcal{S}).$$$

Lean4

theorem isOpen_sUnion (s : Set (Set α)) (hs : ∀ t ∈ s, IsOpen α t) : IsOpen α (⋃₀ s) :=
  by
  simp only [IsOpen] at hs ⊢
  convert CompleteLattice.ωScottContinuous.sSup hs
  aesop

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