mem_pathComponentIn_self

Mathlib.Topology.Connected.PathConnected

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

English

If x belongs to F, then x lies in the path component of x inside F.

Русский

Если x принадлежит F, то x лежит в компоненте пути x внутри F.

LaTeX

$$$$x \in F \Rightarrow x \in \operatorname{pathComponentIn} F x.$$$

Lean4

theorem mem_pathComponentIn_self (h : x ∈ F) : x ∈ pathComponentIn F x :=
  JoinedIn.refl h

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

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

Разделы

Аффилиация

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