arrowCongr_comp — Mathlib

English

Compatibility of arrowCongr with composition: arrowCongr ea ec (g ∘ f) = arrowCongr eb ec g ∘ arrowCongr ea eb f.

Русский

Совместимость arrowCongr с композициями: arrowCongr ea ec (g ∘ f) = arrowCongr eb ec g ∘ arrowCongr ea eb f.

LaTeX

$$$\text{arrowCongr } ea ec (g \circ f) = \text{arrowCongr } eb ec g \circ \text{arrowCongr } ea eb f$$$

Lean4

theorem arrowCongr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁)
    (g : β₁ → γ₁) : arrowCongr ea ec (g ∘ f) = arrowCongr eb ec g ∘ arrowCongr ea eb f := by grind

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