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⟩