map_id — Mathlib

English

For any closed submodule s of M, applying the identity continuous linear map leaves it unchanged: map id s = s.

Русский

Для любого замкнутого подмодуля s в M образ тождественного непрерывного линейного отображения равен самому s.

LaTeX

$$$ClosedSubmodule.map(\mathrm{id}_{R} , s) = s$$$

Lean4

@[simp]
theorem map_id [ContinuousAdd M] [ContinuousConstSMul R M] (s : ClosedSubmodule R M) : s.map (.id _ _) = s :=
  SetLike.coe_injective <| by simpa [map] using s.isClosed.closure_eq

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