instTopologicalSpaceEuclideanHalfSpace

English

The topology on the EuclideanHalfSpace n is the subspace topology inherited from the ambient Euclidean space ℝ^{Fin n}.

Русский

Топология на полупространстве Евклидового типа определяется как подпространственная топология, восходящая к нормальной топологии ℝ^{Fin n}.

LaTeX

$$$$\tau_{H} = \tau_{\mathbb{R}^{\mathrm{Fin}(n)}}\restriction_{H},$$ where $H = \{ x \in \mathbb{R}^{\mathrm{Fin}(n)} : x_i \ge 0 \text{ for all } i \}.$$$

Lean4

instance [NeZero n] : TopologicalSpace (EuclideanHalfSpace n) :=
  instTopologicalSpaceSubtype

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