map_valEmbedding_Icc — Mathlib

English

Applying the nat-embedding to the closed Fin-interval Icc(a,b) yields the Nat-interval Icc(a.val,b.val).

Русский

Применение отображения в натуральные числа к замкнутому Fin-интервалу Icc(a,b) даёт Nat-интервал Icc(a.val,b.val).

LaTeX

$$$(\operatorname{Finset.Icc}\ a\ b).\mathrm{map}\ \mathrm{valEmbedding} = \operatorname{Finset.Icc}(a.\mathrm{val}, b.\mathrm{val})$$$

Lean4

@[simp]
theorem map_valEmbedding_Icc : (Icc a b).map Fin.valEmbedding = Icc (a : ℕ) b :=
  map_valEmbedding_attachFin _

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