genericPoint_closure_eq — Mathlib

English

The closure of the singleton {genericPoint(S)} equals the closure of S for irreducible S.

Русский

Замыкание множества {генерирующая_точка(S)} равно замыканию S при неразложимости S.

LaTeX

$$$\\overline{\\{h_S.genericPoint\\}} = \\overline{S}.$$$

Lean4

@[simp]
theorem genericPoint_closure_eq [QuasiSober α] {S : Set α} (hS : IsIrreducible S) :
    closure ({ hS.genericPoint } : Set α) = closure S :=
  hS.isGenericPoint_genericPoint_closure

Похожие утверждения