subset_pathComponent

Mathlib.Topology.Connected.PathConnected

URI: https://scilib.ai/kg/mathlib#IsPathConnected.subset_pathComponent

English

If F is path-connected, then F is contained in the path component of any x ∈ F.

Русский

Если F связано по траекториям, то F ⊆ pathComponent(x) для любого x ∈ F.

LaTeX

$$$$\forall x\in F:\ F \subseteq \operatorname{pathComponent}(x).$$$$

Lean4

theorem subset_pathComponent (h : IsPathConnected F) (x_in : x ∈ F) : F ⊆ pathComponent x := fun _y y_in =>
  h.mem_pathComponent x_in y_in

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

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

Разделы

Аффилиация

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