English
If X has an open cover U by opens and each U_i is prespectral, then X is prespectral.
Русский
Если X имеет открытое покрытие U из открытых множеств и каждый U_i — prespectral, то X — prespectral.
LaTeX
$$$\\forall i, \\mathrm{PrespectralSpace}(U_i) \\implies \\mathrm{PrespectralSpace}(X)$, где $U$ образует открытое покрытие пространства X.$$
Lean4
theorem of_isOpenCover {ι : Type*} {U : ι → Opens X} (hU : IsOpenCover U) [∀ i, PrespectralSpace (U i)] :
PrespectralSpace X :=
by
refine .of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_
simp only [Set.mem_iUnion, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp, forall_comm (α := Set _),
forall_apply_eq_imp_iff₂]
exact fun i V hV hV' ↦ hV'.image continuous_subtype_val
