homEquiv_comp — Mathlib

English

For CatEnrichedOrdinary C, homEquiv respects composition: homEquiv (f ≫ g) = homEquiv f ≫ homEquiv g.

Русский

Для CatEnrichedOrdinary C отображение гомоморфизмов сохраняет композицию: homEquiv (f ≫ g) = homEquiv f ≫ homEquiv g.

LaTeX

$$$ homEquiv( f \\gg g ) = homEquiv(f) \\;\\gg\\; homEquiv(g) $$$

Lean4

theorem homEquiv_comp {a b c : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) :
    homEquiv (f ≫ g) = homEquiv f ≫ homEquiv g := by
  unfold homEquiv
  simp only [Equiv.trans_apply]
  rw [eHomEquiv_comp]
  rfl

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