mem_pathComponent_iff

Mathlib.Topology.Connected.PathConnected

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

English

For any y, x ∈ X, x ∈ pathComponent y if and only if Joined y x.

Русский

Для любых x,y в X, x принадлежит компоненте пути y тогда и только тогда, когда сопоставимый путь существует, i.e., Joined y x.

LaTeX

$$x ∈ pathComponent y ↔ Joined y x$$

Lean4

theorem mem_pathComponent_iff : x ∈ pathComponent y ↔ Joined y x :=
  .rfl

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

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

Разделы

Аффилиация

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