isGenericPoint_def — Mathlib

English

Let x be a point and S a subset. Then x is a generic point of S if and only if the closure of {x} equals S.

Русский

Пусть x — точка, а S — подмножество. Тогда x является обобщенной точкой S тогда и только тогда, когда замыкание {x} равно S.

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \iff \overline{\{x\}} = S$$$

Lean4

theorem isGenericPoint_def {x : α} {S : Set α} : IsGenericPoint x S ↔ closure ({ x } : Set α) = S :=
  Iff.rfl

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