subset_pathComponentIn — Mathlib

English

If s is path-connected and s ⊆ F with x ∈ s, then s ⊆ pathComponentIn F x.

Русский

Если s связано по траекториям и s ⊆ F, с x ∈ s, то s ⊆ pathComponentIn F x.

LaTeX

$$$$s \text{ path-connected},\ s \subseteq F,\ x\in s \Rightarrow s\subseteq \operatorname{pathComponentIn} F x.$$$$

Lean4

theorem subset_pathComponentIn {s : Set X} (hs : IsPathConnected s) (hxs : x ∈ s) (hsF : s ⊆ F) :
    s ⊆ pathComponentIn F x := fun y hys ↦ (hs.joinedIn x hxs y hys).mono hsF

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