genericPoint_specializes — Mathlib

English

A generic point of a sober irreducible space specializes to every point of the space.

Русский

Генерирующая точка в безраздельном пространстве специализируется на каждую точку пространства.

LaTeX

$$$\\forall x \\in \\alpha,\\; Specializes(genericPoint(\\alpha), x).$$$

Lean4

theorem genericPoint_specializes [QuasiSober α] [IrreducibleSpace α] (x : α) : genericPoint α ⤳ x :=
  (IsIrreducible.isGenericPoint_genericPoint_closure _).specializes (by simp)

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