English
If every member of an open cover is quasi-sober, then the whole space is quasi-sober.
Русский
Если каждый элемент открытого покрытия квазисоберен, то и всё пространство квазисоберно.
LaTeX
$$$S = \\bigcup_i U_i,\\; (\\forall i, \\text{QuasiSober}(U_i)) \\Rightarrow \\text{QuasiSober}(\\alpha).$$$
Lean4
/-- A space is quasi-sober if it can be covered by open quasi-sober subsets. -/
theorem quasiSober_of_open_cover (S : Set (Set α)) (hS : ∀ s : S, IsOpen (s : Set α)) [∀ s : S, QuasiSober s]
(hS' : ⋃₀ S = ⊤) : QuasiSober α :=
TopologicalSpace.IsOpenCover.quasiSober (U := fun s : S ↦ ⟨s, hS s⟩) <| by
simpa [TopologicalSpace.IsOpenCover, ← SetLike.coe_set_eq, sUnion_eq_iUnion] using hS'
