EuclideanQuadrant — Mathlib

English

Let n ≥ 1. The Euclidean quadrant in R^n is the set of vectors with nonnegative coordinates, i.e. { x ∈ R^n : x_i ≥ 0 for all i }. It models manifolds with corners.

Русский

Пусть n ≥ 1. Евклидово квадрант в ℝ^n — множество векторов с неотрицательными координатами: x_i ≥ 0 для всех i. Используется для моделирования многообразий с углами.

LaTeX

$$$$Q_n = \{ x \in \mathbb{R}^{n} \mid x_i \ge 0 \text{ for all } i \}.$$ \\ \\ x = y \iff x_i = y_i \text{ for all } i.$$

Lean4

/-- The quadrant in `ℝ^n`, used to model manifolds with corners, made of all vectors with nonnegative
coordinates.
-/
def EuclideanQuadrant (n : ℕ) : Type :=
  { x : EuclideanSpace ℝ (Fin n) // ∀ i : Fin n, 0 ≤ x i }

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