mul_apply — Mathlib

English

The set of continuous linear endomorphisms M1 →L[R1] M1 carries a MonoidWithZero structure with multiplication given by composition, zero as the zero map, and one as the identity map.

Русский

Множество непрерывных линейных эндоморфизмов M1 →L[R1] M1 образует структуру MonoidWithZero: умножение задаётся композиции, ноль — нулевое отображение, единица — тождественное отображение.

LaTeX

$$$ (f * g) = f \circ g, \; 0 \text{ is the zero map}, \; 1 \text{ is the identity map}$$$

Lean4

theorem mul_apply (f g : M₁ →L[R₁] M₁) (x : M₁) : (f * g) x = f (g x) :=
  rfl

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