comp_eq — Mathlib

English

The two ways of composing f with g and h via the ‘ofHom’ construction coincide: f ∘ g = f ∘ h.

Русский

Два способа композиции f с g и h через конструкцию ofHom совпадают: f ∘ g = f ∘ h.

LaTeX

$$$$ f \circ g = f \circ h. $$$$

Lean4

theorem comp_eq : (f ≫ ofHom g) = f ≫ ofHom h := by
  ext a
  simp only [hom_comp, hom_ofHom, MonoidHom.coe_comp, Function.comp_apply]
  have : f a ∈ {b | h b = g b} := by
    rw [← agree]
    use a
  rw [this]

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