sumCongr_one_swap — Mathlib

English

For i,j ∈ β, sumCongr 1 (swap i j) equals swap on the right embedded: swap (Sum.inr i) (Sum.inr j).

Русский

Для i,j ∈ β, sumCongr 1 (swap i j) = swap (Sum.inr i) (Sum.inr j).

LaTeX

$$$$sumCongr (1 : Perm \\alpha) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j).$$$$

Lean4

@[simp]
theorem sumCongr_one_swap {α β : Type*} [DecidableEq α] [DecidableEq β] (i j : β) :
    sumCongr (1 : Perm α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j) :=
  sumCongr_refl_swap i j

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