map_castAddEmb_Iio — Mathlib

English

Let n,m be natural numbers and i ∈ Fin n. Then the image of the initial interval Iio(i) under the embedding Fin n → Fin(n+m) that adds m to each entry is exactly Iio(castAdd m i).

Русский

Пусть n, m — натуральные числа и i ∈ Fin n. Тогда образ начального отрезка Iio(i) под вложением Fin n → Fin(n+m), полученным прибавлением m к каждому элементу, равен Iio (castAdd m i).

LaTeX

$$$$ \operatorname{Finset.map}(\operatorname{Fin.castAddEmb}(m), \operatorname{Finset.Iio}(i)) = \operatorname{Finset.Iio}(\operatorname{Fin.castAdd} m\, i) $$$$

Lean4

@[simp]
theorem map_castAddEmb_Iio (m) (i : Fin n) : (Iio i).map (castAddEmb m) = Iio (castAdd m i) :=
  map_castLEEmb_Iio ..

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