finsetImage_castLE_Icc — Mathlib

English

Under a length-increasing cast, a closed Fin interval maps to the corresponding closed interval of the casted endpoints.

Русский

При отображении castLE более длинного промежутка финального типа в исходный он отображается в соответствующий замкнутый интервал концов.

LaTeX

$$$(Icc\ a\ b).\mathrm{image}(\mathrm{castLE}\ h) = Icc(\mathrm{castLE}\ h\ a)(\mathrm{castLE}\ h\ b)$$

Lean4

@[simp]
theorem finsetImage_castLE_Icc (h : n ≤ m) : (Icc a b).image (castLE h) = Icc (castLE h a) (castLE h b) := by
  simp [← coe_inj]

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