instZeroEuclideanHalfSpace

Mathlib.Geometry.Manifold.Instances.Real

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

English

The origin belongs to EuclideanHalfSpace n, i.e. the vector with all coordinates zero lies in the half-space.

Русский

Происходит включение начала координат в полупространство: вектор нулей принадлежит полупространству.

LaTeX

$$$$\mathbf{0} = (0,\dots,0) \in H_n^+.$$$$

Lean4

instance {n : ℕ} [NeZero n] : Zero (EuclideanHalfSpace n) :=
  ⟨⟨fun _ ↦ 0, by simp⟩⟩

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

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

Разделы

Аффилиация

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