isPathConnected_pathComponentIn — Mathlib

English

If x ∈ F, then pathComponentIn F x is path-connected.

Русский

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

LaTeX

$$$$\text{If } x \in F,\ \operatorname{IsPathConnected}(\operatorname{pathComponentIn} F x).$$$$

Lean4

theorem isPathConnected_pathComponentIn (h : x ∈ F) : IsPathConnected (pathComponentIn F x) :=
  ⟨x, mem_pathComponentIn_self h, fun _ ⟨γ, hγ⟩ ↦
    by
    refine ⟨γ, fun t ↦ ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
    dsimp [Path.truncateOfLE, Path.truncate]
    exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _⟩

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