isGenericPoint_genericPoint — Mathlib

English

For an irreducible S, the generic point of closure S has a defining property: it is a generic point for closure S.

Русский

Для неразложимого S геометрическая точка замыкания имеет свойство быть генерирующей точкой для замыкания S.

LaTeX

$$$\\text{If } h_S \\text{ is irreducible, then } IsGenericPoint(h_S.genericPoint, closure(S)).$$$

Lean4

theorem isGenericPoint_genericPoint [QuasiSober α] {S : Set α} (hS : IsIrreducible S) (hS' : IsClosed S) :
    IsGenericPoint hS.genericPoint S := by convert hS.isGenericPoint_genericPoint_closure; exact hS'.closure_eq.symm

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