closure_genericPoint — Mathlib

English

If S is irreducible and closed, then the closure of the generic point of S is S itself.

Русский

Если S неразложимо и замкнуто, то замыкание генерирующей точки S равно самому S.

LaTeX

$$$\\overline{\\{h_S.genericPoint\\}} = S \\quad \\text{when } IsClosed(S).$$$

Lean4

theorem closure_genericPoint [QuasiSober α] {S : Set α} (hS : IsIrreducible S) (hS' : IsClosed S) :
    closure ({ hS.genericPoint } : Set α) = S :=
  hS.isGenericPoint_genericPoint_closure.trans hS'.closure_eq

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