specializes_refl

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#specializes_refl

English

Let X be a topological space and x be a point of X. Then x specializes to itself.

Русский

Пусть X — топологическое пространство и x — точка в X. Тогда x специализируется на себе самом.

LaTeX

$$$$\forall X\ [\text{TopologicalSpace } X],\ \forall x:X,\ x \rightsquigarrow x.$$$$

Lean4

@[refl]
theorem specializes_refl (x : X) : x ⤳ x :=
  specializes_rfl

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

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

Разделы

Аффилиация

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