toContinuousAddMonoidHom_inj — Mathlib

English

The map sending a continuous linear map to a ContinuousAddMonoidHom is injective.

Русский

Отображение, переводящее непрерывное линейное отображение в ContinuousAddMonoidHom, инъективно.

LaTeX

$$Injective ((↑) : (M_1 →SL[σ_{12}] M_2) → ContinuousAddMonoidHom M_1 M_2)$$

Lean4

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_inj {f g : M₁ →SL[σ₁₂] M₂} : (f : ContinuousAddMonoidHom M₁ M₂) = g ↔ f = g :=
  toContinuousAddMonoidHom_injective.eq_iff

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