comp_one — Mathlib

English

Another form of identity under composition: composing with the identity yields a constant function at the image of 1.

Русский

Ещё одна форма тождества в композиции: композиция с единицей даёт константную функцию на образе единицы.

LaTeX

$$g.comp (1 : C(α, β)) = const α (g 1)$$

Lean4

@[to_additive (attr := simp)]
theorem comp_one [One β] (g : C(β, γ)) : g.comp (1 : C(α, β)) = const α (g 1) :=
  rfl

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