instTopologicalSpace — Mathlib

English

The same topological space structure is placed on Mᵈᵐᵃ as on M, via the induced topology from mk.symm.

Русский

На M^{d m a} устанавливается та же топология, что и на M, через индуцированную топологию от mk.symm.

LaTeX

$$$TopologicalSpace\, M^{\mathrm{d}\mathrm{m}\mathrm{a}} = \, \operatorname{induced} (mk.symm) (TopologicalSpace M)$$$

Lean4

/-- Put the same topological space structure on `Mᵈᵐᵃ` as on the original space. -/
@[to_additive /-- Put the same topological space structure on `Mᵈᵃᵃ` as on the original space. -/
    ]
instance instTopologicalSpace : TopologicalSpace Mᵈᵐᵃ :=
  .induced mk.symm ‹_›

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