sumCongr_refl — Mathlib

English

The sumCongr of identity equivalences equals the identity on the sum: (refl α).sumCongr (refl β) = refl (α ⊕ β).

Русский

Суммарное соответствие эйлевских единиц равно единице на сумме: (refl α).sumCongr (refl β) = refl (α ⊕ β).

LaTeX

$$Equiv.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)$$

Lean4

@[simp]
theorem sumCongr_refl {α β} : Equiv.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β) :=
  by
  ext i
  cases i <;> rfl

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