English
Let n ≥ 1. The Euclidean half-space in R^n consists of all vectors with nonnegative coordinates, i.e. { x ∈ R^n : x_i ≥ 0 for all i } and serves as a prototype for manifolds with boundary.
Русский
Пусть n ≥ 1. Евклидово полупространство в ℝ^n состоит из всех векторов с неотрицательными координатами, то есть { x ∈ ℝ^n : x_i ≥ 0 для всех i }, и служит моделью для многообразий с границей.
LaTeX
$$$$H_n^+ = \{ x \in \mathbb{R}^{n} \mid x_i \ge 0 \text{ for all } i = 1,\dots,n \}.$$$$
Lean4
/-- The half-space in `ℝ^n`, used to model manifolds with boundary. We only define it when
`1 ≤ n`, as the definition only makes sense in this case.
-/
def EuclideanHalfSpace (n : ℕ) [NeZero n] : Type :=
{ x : EuclideanSpace ℝ (Fin n) // 0 ≤ x 0 }
