instLocPathConnectedSpaceEuclideanHalfSpace

Mathlib.Geometry.Manifold.Instances.Real

URI: https://scilib.ai/kg/mathlib#instLocPathConnectedSpaceEuclideanHalfSpace

English

The Euclidean half-space is locally path-connected (for NeZero n).

Русский

Полупространство Евклида локально путь-соединённое (для NeZero n).

LaTeX

$$$\\forall n \\in \\mathbb{N}, [\\mathrm{NeZero}\\; n] \\Rightarrow \\mathrm{LocPathConnectedSpace}(\\mathrm{EuclideanHalfSpace}(n))$$$

Lean4

instance [NeZero n] : LocPathConnectedSpace (EuclideanHalfSpace n) :=
  EuclideanHalfSpace.convex.locPathConnectedSpace

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru