coe_comp — Mathlib

English

The coercion of the composition equals the composition of the coerced maps: the embedded form of g∘f equals the composition of the embeds of g and f.

Русский

Сведение композиции к функциям совпадает с композицией вложенных отображений: встроенная форма g∘f равна композиции вложений g и f.

LaTeX

$$$ \operatorname{coe}(g \circ f) = \operatorname{coe}(g) \circ \operatorname{coe}(f) $$$

Lean4

@[simp, norm_cast]
theorem coe_comp (g : Copy B C) (f : Copy A B) : ⇑(g.comp f) = g ∘ f := by ext; simp

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