English
If s is locally constructible and s ⊆ t with t compact in a prespectral, quasi-separated space X, then s is constructible.
Русский
Пусть s локально конструируемо, s ⊆ t и t компактно в пространстве X, удовлетворяющем условиям Prespectral и QuasiSeparated. Тогда s является конструируемым.
LaTeX
$$$\\operatorname{IsLocallyConstructible}(s) \\wedge (s\\subseteq t) \\wedge \\operatorname{IsCompact}(t) \\Rightarrow \\operatorname{IsConstructible}(s).$$$
Lean4
theorem isConstructible_of_subset_of_isCompact [PrespectralSpace X] [QuasiSeparatedSpace X]
(hs : IsLocallyConstructible s) (hst : s ⊆ t) (ht : IsCompact t) : IsConstructible s :=
by
have (x : _) : ∃ U, IsOpen U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s) :=
have ⟨U, hxU, hU, hUs⟩ := hs x
have ⟨V, ⟨hV₁, hV₂⟩, hxV, hVU⟩ := PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp hxU
have : IsConstructible (V ↓∩ s) := (hUs.preimage_of_isOpenEmbedding (IsOpenEmbedding.id.restrict hVU hV₁) :)
have : IsConstructible (V ∩ s) :=
by
have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal (by simpa using hV₂.isRetrocompact hV₁)
rwa [Subtype.image_preimage_coe] at this
⟨V, hV₁, hV₂, hxV, this⟩
choose U hU hU' hxU hUs using this
obtain ⟨σ, hσ, htσ⟩ := ht.elim_nhds_subcover U (fun x _ ↦ (hU x).mem_nhds (hxU x))
convert IsConstructible.biUnion σ.finite_toSet (fun x _ ↦ hUs x)
apply subset_antisymm
· rw [← Set.iUnion₂_inter, Set.subset_inter_iff]
exact ⟨hst.trans htσ, subset_rfl⟩
· exact Set.iUnion₂_subset fun _ _ ↦ Set.inter_subset_right
