ι_comp_map — Mathlib

English

If hf and hf' commute in squares, then the composed maps satisfy the two-square relation $(\\psi' ∘ \\psi) ∘ f_1 = f_3 ∘ (φ' ∘ φ)$.

Русский

Если квадраты с hf и hf' коммутизируют, то составные отображения удовлетворяют двумумостной формуле $(\\psi' ∘ \\psi) ∘ f_1 = f_3 ∘ (φ' ∘ φ)$.

LaTeX

$$$(\\psi' ∘ \\psi) ∘ f_1 = f_3 ∘ (φ' ∘ φ)$$$

Lean4

@[simp]
theorem ι_comp_map (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :
    (ι f₂ g₂).comp (map φ ψ hf hg) = φ.comp (ι f₁ g₁) :=
  ι_comp_lift _ _

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