toLocPathConnectedSpace — Mathlib

English

If E is a real-vector-space with a locally convex structure and compatible topology, then E is locally path connected.

Русский

Если E — вещественный векторное пространство с локально выпуклой структурой и совместимой топологией, то E локально путево связно.

LaTeX

$$$\text{LocPathConnectedSpace } E$ (given $E$ is a locally convex real space with appropriate module structure)$$

Lean4

instance (priority := 100) toLocPathConnectedSpace [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] :
    LocPathConnectedSpace E :=
  .of_bases (fun x ↦ convex_basis (𝕜 := ℝ) x) fun _ _ hs ↦
    hs.2.isPathConnected <| nonempty_of_mem <| mem_of_mem_nhds hs.1

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