sumCongr_swap_one — Mathlib

English

For i,j in α, sumCongr (swap i j) (1) equals swap on the left embedded in α: swap on Sum.inl i and Sum.inl j.

Русский

Для i,j ∈ α, sumCongr (swap i j) (1) = swap (Sum.inl i) (Sum.inl j).

LaTeX

$$$$sumCongr (Equiv.swap i j) (1 : Perm \\\\alpha) = Equiv.swap (\\\\text{Sum.inl } i) (\\\\text{Sum.inl } j).$$$$

Lean4

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

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