map_castLEEmb_Iic — Mathlib

English

Let n ≤ m. For any a ∈ Fin n (the variable b is inconsequential here), the image of the downward interval Iic a under the order-embedding castLEEmb h is exactly the downward interval Iic (castLE h a) in Fin m.

Русский

Пусть n ≤ m. Для любого a ∈ Fin n отображение нисходящего интервала Iic a под вложением порядка castLEEmb h равно нисходящему интервалу Iic (castLE h a) в Fin m.

LaTeX

$$$ (\mathrm{Finset}.map (\mathrm{Fin.castLEEmb}\, h)\; (\mathrm{Finset}.Iic\, a)) = (\mathrm{Finset}.Iic\ (\mathrm{Fin.castLE}\, h\, a)) $$$

Lean4

@[simp]
theorem map_castLEEmb_Iic (h : n ≤ m) : (Iic a).map (castLEEmb h) = Iic (castLE h a) := by simp [← coe_inj]

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