isClosedEmbedding_mapGLInt — Mathlib

English

The map GL from SL( n, ℤ ) into GL(n, ℝ) is a closed embedding.

Русский

Отображение GL из SL(n,ℤ) в GL(n,ℝ) является замкнутым вложением.

LaTeX

$$Topology.IsClosedEmbedding (mapGL ℝ : SL n ℤ → GL n ℝ)$$

Lean4

theorem isClosedEmbedding_mapGLInt : Topology.IsClosedEmbedding (mapGL ℝ : SL n ℤ → GL n ℝ) :=
  ⟨isEmbedding_mapGL (Isometry.isEmbedding fun _ _ ↦ rfl), (mapGL ℝ).range.isClosed_of_discrete⟩

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