English
Let X be a topological space and F a subset of X. If there exists a continuous map f: [0,1] → X with f(0) = x, f(1) = y, and f([0,1]) ⊆ F, then x and y are joined in F (i.e., there is a path in F from x to y).
Русский
Пусть X — топологическое пространство, F ⊆ X. Если существует непрерывное отображение f: [0,1] → X such that f(0) = x, f(1) = y и f([0,1]) ⊆ F, то x и y соединены в F (существует путь в F от x до y).
LaTeX
$$$\\exists f: I \\to X\\ (ContinuousOn\\ f\\ I\\land f(0)=x\\land f(1)=y\\land f(I)\\subseteq F) \\Rightarrow JoinedIn F x y$$$
Lean4
theorem ofLine {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) (hF : f '' I ⊆ F) : JoinedIn F x y :=
⟨Path.ofLine hf h₀ h₁, fun t => hF <| Path.ofLine_mem hf h₀ h₁ t⟩
