English
If ρ: E → A is a continuous surjection and the Zorn-subset condition holds, then the image ρ''G of any open set G is contained in the closure of the complement of ρ''E\\G.
Русский
При непрерывном сюрьективном отображении ρ: E → A и выполняющем условие Зорна множество, образ открытого G лежит в замыкании дополнения к образу E\\G.
LaTeX
$$$$ \\rho''G \\subseteq \\overline{(\\rho''E \\setminus \\rho''G)^c} $$ для открытого G и т.д.$$
Lean4
/-- Lemma 2.1 in [Gleason, *Projective topological spaces*][gleason1958]:
if $\rho$ is a continuous surjection from a topological space $E$ to a topological space $A$
satisfying the "Zorn subset condition", then $\rho(G)$ is contained in
the closure of $A \setminus \rho(E \setminus G)$ for any open set $G$ of $E$. -/
theorem image_subset_closure_compl_image_compl_of_isOpen {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : ρ.Surjective)
(zorn_subset : ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ) {G : Set E} (hG : IsOpen G) :
ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ) := by
-- suffices to prove for nonempty $G$
by_cases G_empty : G = ∅
· simpa only [G_empty, image_empty] using empty_subset _
· -- let $a \in \rho(G)$
intro a ha
rw [mem_closure_iff]
-- let $N$ be a neighbourhood of $a$
intro N N_open hN
rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
have nonempty : (G ∩ ρ ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr hN⟩
have is_open : IsOpen <| G ∩ ρ ⁻¹' N := hG.inter <| N_open.preimage ρ_cont
have ne_univ : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ univ := zorn_subset _ (compl_ne_univ.mpr nonempty) is_open.isClosed_compl
rcases nonempty_compl.mpr ne_univ with
⟨x, hx⟩
-- prove $x \in N \cap (A \setminus \rho(E \setminus G))$
have hx' : x ∈ (ρ '' Gᶜ)ᶜ := fun h => hx <| image_mono (by simp) h
rcases ρ_surj x with ⟨y, rfl⟩
have hy : y ∈ G ∩ ρ ⁻¹' N := by simpa using mt (mem_image_of_mem ρ) <| mem_compl hx
exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩
