coe_comp — Mathlib

English

The coercion of the composition equals the composition of coercions with lifted functions: ((g ∘ f) : α →. γ) = (g : β →. γ).comp f.

Русский

Приведение композиции равно композиции приведения с поднятыми функциями: (g ∘ f) = g ∘ f.

LaTeX

$$$$ ((g \circ f : \alpha \to. \gamma) : \alpha \to. \gamma) = (g : \beta \to. \gamma).comp f. $$$$

Lean4

theorem coe_comp (g : β → γ) (f : α → β) : ((g ∘ f : α → γ) : α →. γ) = (g : β →. γ).comp f :=
  ext fun _ _ => by simp only [coe_val, comp_apply, Function.comp, Part.bind_some]

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