compPMap_apply — Mathlib

English

The value of the composed partial map at x is obtained by first applying f and then applying g: (g ∘_P f)(x) = g(f(x)) for x in dom(f).

Русский

Значение частично заданного отображения, полученного после композиции, в точке x задаётся как g(f(x)) при x ∈ dom(f).

LaTeX

$$$(g \circ_P f)(x) = g(f(x))\quad(x\in\operatorname{dom}(f)).$$$

Lean4

@[simp]
theorem compPMap_apply (g : F →ₗ[R] G) (f : E →ₗ.[R] F) (x) : g.compPMap f x = g (f x) :=
  rfl

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