range_euclideanQuadrant — Mathlib

English

The range of the projection from EuclideanHalfSpace n is the set { y | y_0 ≥ 0 }.

Русский

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

LaTeX

$$$\\mathrm{range}(\\mathrm{Subtype}.val : \\mathrm{EuclideanHalfSpace}(n) \\to _) = \\{ y : y_0 \\ge 0 \\}$$$

Lean4

theorem range_euclideanQuadrant (n : ℕ) : range (Subtype.val : EuclideanQuadrant n → _) = {y | ∀ i : Fin n, 0 ≤ y i} :=
  Subtype.range_val

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