finSumEquivOfFinset_inr — Mathlib

English

For hm: #s = m and hn: #sᶜ = n and i ∈ Fin n, the image of Sum.inr i under finSumEquivOfFinset is sᶜ.orderEmbOfFin hn i.

Русский

При hm: #s = m, hn: #sᶜ = n и i ∈ Fin n, образ Sum.inr i через finSumEquivOfFinset равен sᶜ.orderEmbOfFin hn i.

LaTeX

$$$finSumEquivOfFinset hm hn (Sum.inr i) = sᶜ.orderEmbOfFin hn i$$$

Lean4

@[simp]
theorem finSumEquivOfFinset_inr (hm : #s = m) (hn : #sᶜ = n) (i : Fin n) :
    finSumEquivOfFinset hm hn (Sum.inr i) = sᶜ.orderEmbOfFin hn i :=
  rfl

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