sumCongr_refl — Mathlib

English

The sum-congruence of identity maps is the identity on the sum: sumCongr (refl α) (refl β) = refl (Sum α β).

Русский

Суммовая конгруэнтность тождественных отображений есть тождественное отображение на сумме: sumCongr (refl α) (refl β) = refl (Sum α β).

LaTeX

$$$\text{sumCongr}(.\mathrm{refl}\, \alpha)(.\mathrm{refl}\, \beta) = .\mathrm{refl}\ _ $$$

Lean4

@[simp]
theorem sumCongr_refl : sumCongr (.refl α) (.refl β) = .refl _ := by ext; simp

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