pathConnectedSpace — Mathlib

English

For every n ≥ 1, the Euclidean half-space { x ∈ R^n | x_1 ≥ 0 } is path-connected.

Русский

Для каждого n ≥ 1 полупространство Евклида { x ∈ R^n | x_1 ≥ 0 } является путь-соединённым.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ n>0:\\; \\text{PathConnected}(\\{ x \\in \\mathbb{R}^n \\mid x_1 \\ge 0\\})$$$

Lean4

instance pathConnectedSpace [NeZero n] : PathConnectedSpace (EuclideanHalfSpace n) :=
  isPathConnected_iff_pathConnectedSpace.mp <| convex.isPathConnected ⟨0, by simp⟩

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