map_zero

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.map_zero

English

Reiterates that the image-closure relation holds for continuous linear equivalences.

Русский

Повторение утверждения о замыкании образа для непрерывных линейных эквивалентностей.

LaTeX

$$$ e '' closure(S) = closure(e''S) $$$

Lean4

theorem map_zero (e : M₁ ≃SL[σ₁₂] M₂) : e (0 : M₁) = 0 :=
  (e : M₁ →SL[σ₁₂] M₂).map_zero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru