sumCongr_trans — Mathlib

English

The composition of sumCongr respects transitivity: (e.sumCongr f).trans (g.sumCongr h) equals (e.trans g).sumCongr (f.trans h).

Русский

Составление sumCongr сохраняет переходы: (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h).

LaTeX

$$ (Equiv.sumCongr e f).trans (Equiv.sumCongr g h) = Equiv.sumCongr (e.trans g) (f.trans h)$$

Lean4

@[simp]
theorem sumCongr_trans {α₁ α₂ β₁ β₂ γ₁ γ₂} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) :
    (Equiv.sumCongr e f).trans (Equiv.sumCongr g h) = Equiv.sumCongr (e.trans g) (f.trans h) :=
  by
  ext i
  cases i <;> rfl

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