Connected_Open_Subset_of_Euclidean_Space_is_Path_Connected
Provedconnected-spacespath-connected-spacesproofwikitopology
Let U be a connected open subset of Euclidean n-space. Then U is path-connected.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Connected.PathConnected
Formal statement
theorem Connected_Open_Subset_of_Euclidean_Space_is_Path_Connected {n : ℕ} {U : Set (Fin n → ℝ)} (hU_open : IsOpen U) (hU_conn : IsConnected U) : IsPathConnected U := by sorrySource