of_comp_eq_base — Mathlib

English

For every i, the two ways around the square commute: the i-th inclusion composed with φ_i equals the base map.

Русский

Для каждого i диаграмма замкнута: (of_i) ∘ φ_i = base φ.

LaTeX

$$$(\;of_i\; ) \circ (\phi_i) = base(\varphi)\quad \text{for all } i$$$

Lean4

theorem of_comp_eq_base (i : ι) : (of i).comp (φ i) = (base φ) :=
  by
  ext x
  apply (Con.eq _).2
  refine ConGen.Rel.of _ _ ?_
  simp only [MonoidHom.comp_apply]
  exact ⟨_, _, rfl, rfl⟩

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