English
If X is prespectral and f: X → Y is open, then for suitable open U in Y contained in range f there exists an open V in X with f''V = U and V compact.
Русский
Если X prespectral и f: X → Y открытое отображение, тогда существование открытого V в X с свойством f''V = U и V компактно для подходящего U в Y.
LaTeX
$$$[\\text{PrespectralSpace}(X)] \\land f\\text{ open} \\Rightarrow \\forall U\\subseteq \\mathrm{range}(f): \\ \\text{IsOpen}(U) \\land \\text{IsCompact}(U) \\Rightarrow \\exists V:\\ Opens(X), \\text{IsCompact}(V.1) \\land f''V = U$$$
Lean4
/-- If `X` has a basis of compact opens and `f : X → S` is open, every
compact open of `S` is the image of a compact open of `X`. -/
theorem exists_opens_image_eq_of_prespectralSpace [PrespectralSpace X] {f : X → Y} (hfc : Continuous f)
(h : IsOpenMap f) {U : Set Y} (hs : U ⊆ Set.range f) (hU : IsOpen U) (hc : IsCompact U) :
∃ (V : Opens X), IsCompact V.1 ∧ f '' V = U :=
by
obtain ⟨Us, hUs, heq⟩ :=
TopologicalSpace.Opens.isBasis_iff_cover.mp (PrespectralSpace.isBasis_opens X) ⟨f ⁻¹' U, hU.preimage hfc⟩
obtain ⟨t, ht⟩ :=
by
refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)
obtain ⟨x, rfl⟩ := hs hx
obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]
exact Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩
refine ⟨⨆ s ∈ t, s.1, ?_, ?_⟩
· simp only [iSup_mk, carrier_eq_coe, coe_mk]
exact t.finite_toSet.isCompact_biUnion fun i _ ↦ hUs i.2
· simp only [iSup_mk, carrier_eq_coe, Set.iUnion_coe_set, coe_mk, Set.image_iUnion]
convert_to ⋃ i ∈ t, f '' i.1 = U
· simp
· refine subset_antisymm (fun x ↦ ?_) ht
simp_rw [Set.mem_iUnion]
rintro ⟨i, hi, x, hx, rfl⟩
have := heq ▸ mem_sSup.mpr ⟨i.1, i.2, hx⟩
exact this
