instTopologicalSpace

Mathlib.Topology.Instances.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.instTopologicalSpace

English

The topology on SL(n,R) is the subspace topology inherited from GL(n,R).

Русский

Топология на SL(n,R) является подпостроенной (subspace) топологией, унаследованной от GL(n,R).

LaTeX

$$TopologicalSpace(SL(n,R)) = TopologicalSpace(GL(n,R))|_SL(n,R)$$

Lean4

instance : TopologicalSpace (SpecialLinearGroup n R) :=
  instTopologicalSpaceSubtype

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru