comm_sq₂ — Mathlib

English

If ψ∘f1 = f2∘φ and ψ'∘f2 = f3∘φ', then (ψ'∘ψ)∘f1 = f3∘(φ'∘φ).

Русский

Пусть выполняются равенства ψ∘f1 = f2∘φ и ψ'∘f2 = f3∘φ'; тогда (ψ'∘ψ)∘f1 = f3∘(φ'∘φ).

LaTeX

$$$ (\psi'\circ \psi)\circ f_1 = f_3\circ (\phi'\circ \phi). $$$

Lean4

theorem comm_sq₂ (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :
    (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ) := by rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]

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