modelWithCornersEuclideanHalfSpace_zero

Mathlib.Geometry.Manifold.Instances.Real

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

English

The range of the corner-model map at zero is { y | 0 ≤ y_0 }.

Русский

Образ отображения модели с углами на нуле равен полупространству { y | y_0 ≥ 0 }.

LaTeX

$$$\\mathrm{range}(\\mathcal{R}\\partial_n) = \\{ y : y_0 \\ge 0 \\}$$$

Lean4

theorem modelWithCornersEuclideanHalfSpace_zero {n : ℕ} [NeZero n] : (𝓡∂ n) 0 = 0 :=
  rfl

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

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

Разделы

Аффилиация

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