mem_pathComponent_of_mem

Mathlib.Topology.Connected.PathConnected

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

English

If x ∈ pathComponent y, then y ∈ pathComponent x.

Русский

Если x принадлежит pathComponent y, то y принадлежит pathComponent x.

LaTeX

$$x ∈ pathComponent y → y ∈ pathComponent x$$

Lean4

theorem mem_pathComponent_of_mem (h : x ∈ pathComponent y) : y ∈ pathComponent x :=
  Joined.symm h

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

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

Разделы

Аффилиация

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