English
Let n ≤ m. For any a ∈ Fin n, the image under castLEEmb h of the interval Iio a equals Iio (castLE h a).
Русский
Пусть n ≤ m. Отображение под вложением порядка castLEEmb h интервала Iio a равно Iio (castLE h a).
LaTeX
$$$ (\mathrm{Finset}.map (\mathrm{Fin.castLEEmb}\, h)\ (\mathrm{Finset}.Iio\, a)) = (\mathrm{Finset}.Iio\ (\mathrm{Fin.castLE}\, h\, a)) $$$
Lean4
@[simp]
theorem map_castLEEmb_Iio (h : n ≤ m) : (Iio a).map (castLEEmb h) = Iio (castLE h a) := by simp [← coe_inj]