English
If f is a closed embedding and the codomain is quasi-sober, then the domain is quasi-sober as well.
Русский
Если отображение является замкнутым вложением и кодоменм пространство квазисобро, то домен тоже квазисоберен.
LaTeX
$$$\\text{QuasiSober}(\\alpha)\\;\\text{whenever } f: \\alpha \\to \\beta \\text{ is a closed embedding and } \\text{QuasiSober}(\\beta).$$$
Lean4
theorem quasiSober {f : α → β} (hf : IsClosedEmbedding f) [QuasiSober β] : QuasiSober α where
sober hS
hS' := by
have hS'' := hS.image f hf.continuous.continuousOn
obtain ⟨x, hx⟩ := QuasiSober.sober hS'' (hf.isClosedMap _ hS')
obtain ⟨y, -, rfl⟩ := hx.mem
use y
apply image_injective.mpr hf.injective
rw [← hx.def, ← hf.closure_image_eq, image_singleton]
