mem

Mathlib.Topology.Sober

URI: https://scilib.ai/kg/mathlib#IsGenericPoint.mem

English

If x is a generic point of S, then x ∈ S.

Русский

Если x — обобщенная точка S, то x принадлежит S.

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \Rightarrow x \in S$$$

Lean4

protected theorem mem (h : IsGenericPoint x S) : x ∈ S :=
  h.specializes_iff_mem.1 specializes_rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru