refl

Mathlib.Topology.Connected.PathConnected

URI: https://scilib.ai/kg/mathlib#Joined.refl

English

For any x in a topological space X, x is joined to itself by the constant path at x.

Русский

Для любого x в пространстве X существует путь из x в x, константный путь.

LaTeX

$$$Joined\;refl(x)$$$

Lean4

@[refl]
theorem refl (x : X) : Joined x x :=
  ⟨Path.refl x⟩

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

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

Разделы

Аффилиация

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