comp_apply — Mathlib

English

For isomorphisms f:A ⟶ B and g:B ⟶ C, the composed morphism corresponds to the composition of the underlying ContinuousMonoidHoms.

Русский

Для изоморфизмов f и g композиция морфизмов соответствует композиции соответствующих непрерывных гомоморфизмов.

LaTeX

$$theorem comp_apply {A B C : ProfiniteGrp} (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a)$$

Lean4

@[to_additive]
theorem comp_apply {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : A) : (f ≫ g) a = g (f a) := by
  simp only [hom_comp, ContinuousMonoidHom.comp_toFun]

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