isClosedEmbedding_toGL — Mathlib

English

The natural inclusion i: SL_n(R) → GL_n(R) is a closed embedding; it is an embedding of topological spaces whose image is a closed subset of GL_n(R).

Русский

Естественное включение i: SL_n(R) → GL_n(R) является замкнутым вложением; образ гомоморфизма является замкнутой подмножностью GL_n(R).

LaTeX

$$$IsClosedEmbedding(toGL)$$$

Lean4

/-- The natural inclusion of `SL n A` in `GL n A` is a closed embedding. -/
theorem isClosedEmbedding_toGL [T0Space R] : Topology.IsClosedEmbedding (toGL : SL n R → GL n R) :=
  ⟨isEmbedding_toGL, by simpa [range_toGL] using isClosed_singleton.preimage <| by fun_prop⟩

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