mem_pathComponent_self

Mathlib.Topology.Connected.PathConnected

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

English

Every point x is joined to itself, hence x ∈ pathComponent x.

Русский

Каждая точка x соединена сама с собой; следовательно, x ∈ pathComponent x.

LaTeX

$$x ∈ pathComponent x$$

Lean4

@[simp]
theorem mem_pathComponent_self (x : X) : x ∈ pathComponent x :=
  Joined.refl x

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

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

Разделы

Аффилиация

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