funLeft_apply — Mathlib

English

funLeft maps a function f to a linear map that precomposes by f; applying this to g shows the map is given by g ∘ f.

Русский

funLeft отправляет функцию f в линейное отображение, предварительно композиция с f; применение к g даёт отображение g ∘ f.

LaTeX

$$$ (\mathrm{funLeft}\; R\; M\; f)\; g = g \circ f $$$

Lean4

@[simp]
theorem funLeft_apply (f : m → n) (g : n → M) (i : m) : funLeft R M f g i = g (f i) :=
  rfl

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