range_modelWithCornersEuclideanHalfSpace

English

The range of the corner-model map 𝓡∂ n is the nonnegative first coordinate set.

Русский

Образ отображения модели с углами 𝓡∂ n — это множество с неотрицательной первой координатой.

LaTeX

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

Lean4

theorem range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] : range (𝓡∂ n) = {y | 0 ≤ y 0} :=
  range_euclideanHalfSpace n

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