instTopologicalSpaceEuclideanQuadrant

English

The Euclidean Quadrant is equipped with the subspace topology inherited from the ambient Euclidean space.

Русский

Евклидово квадрантное множество оснащается подпространственной топологией, полученной от окружающего Евклидова пространства.

LaTeX

$$$$\mathcal{T}_{Q_n} = \mathcal{T}_{\mathbb{R}^n} \upharpoonright Q_n.$$$$

Lean4

instance : TopologicalSpace (EuclideanQuadrant n) :=
  instTopologicalSpaceSubtype

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