map_castLEEmb_Iio — Mathlib

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]

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