English
Convex subsets of locally convex spaces are locally path-connected.
Русский
Выпуклые подмножества локально выпуклых пространств локально путево связны.
LaTeX
$$$\\text{Convex } S \\Rightarrow \\text{LocPathConnectedSpace } S$$$
Lean4
/-- Convex subsets of locally convex spaces are locally path-connected. -/
theorem locPathConnectedSpace [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {S : Set E} (hS : Convex ℝ S) :
LocPathConnectedSpace S :=
by
refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩
let ⟨t, ht⟩ := (mem_nhds_subtype S x s).mp hs
let ⟨t', ht'⟩ := (LocallyConvexSpace.convex_basis (𝕜 := ℝ) x.1).mem_iff.mp ht.1
refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩
· exact continuousAt_subtype_val.preimage_mem_nhds ht'.1.1
· refine Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left
exact (hS.inter ht'.1.2).isPathConnected ⟨x, x.2, mem_of_mem_nhds ht'.1.1⟩
