comp_f — Mathlib

English

The nth component of the composite equals the composite of the nth components: (Φ12 ≫ Φ23).f n = Φ12.f n ≫ Φ23.f n.

Русский

Компонента n-го составного равна композиции компонент: (Φ12 ≫ Φ23).f n = Φ12.f n ≫ Φ23.f n.

LaTeX

$$$\big( (\Phi_{12} \gg \Phi_{23}) .f \big)(n) = (\Phi_{12}.f n) \;\circ\; (\Phi_{23}.f n)$$$

Lean4

@[simp]
theorem comp_f {S₁ S₂ S₃ : Split C} (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃) (n : ℕ) : (Φ₁₂ ≫ Φ₂₃).f n = Φ₁₂.f n ≫ Φ₂₃.f n :=
  rfl

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