coe_comp — Mathlib

English

The coercion of the composition equals the composition of the coercions: the underlying function of (f.comp g) is f ∘ g.

Русский

Коэрцирование композиции равно композиции коэрцирований: функция (f.comp g) равна f ∘ g.

LaTeX

$$$\\text{coe}(f.comp g) = \\text{coe}(f) \\circ \\text{coe}(g)$$$

Lean4

@[simp]
theorem coe_comp (f : CocompactMap β γ) (g : CocompactMap α β) : ⇑(comp f g) = f ∘ g :=
  rfl

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