English
Any R1 space is quasi-sober because every irreducible set lies in the closure of a singleton.
Русский
Любое R1-пространство квазисоберно, потому что любая неразложимая множества содержится в замыкании одного элемента.
LaTeX
$$$\\text{R1Space}(\\alpha) \\Rightarrow \\text{QuasiSober}(\\alpha)$, since every irreducible set is contained in closure of a singleton.$$
Lean4
/-- Any R1 space is a quasi-sober space because any irreducible set is
contained in the closure of a singleton.
-/
-- see note [lower instance priority]
instance (priority := 100) quasiSober [R1Space α] : QuasiSober α where
sober h
hs := by
obtain ⟨x, hx⟩ := h.nonempty
use x
apply subset_antisymm
· rw [← hs.closure_eq]
exact closure_mono (singleton_subset_iff.mpr hx)
· exact isPreirreducible_iff_forall_mem_subset_closure_singleton.mp h.isPreirreducible x hx
