finSumEquivOfFinset_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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