apply — Mathlib

English

A simp/norm_cast version: the map to ContinuousAddMonoidHom is injective when restricted to ContinuousLinearMap.

Русский

Упрощённая версия: отображение в ContinuousAddMonoidHom инъективно на множестве ContinuousLinearMap.

LaTeX

$$$\mathrm{toContinuousAddMonoidHom\_inj} : (f\mapsto \mathrm{toContinuousAddMonoidHom}(f))$ is injective$$

Lean4

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def apply (h : M₁ →SL[σ₁₂] M₂) : M₁ → M₂ :=
  h

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