English
In Fin type, finset image under castLE preserves uIcc structure, i.e., finset image of uIcc under castLE equals uIcc of the images.
Русский
В типе Fin отображение через castLE сохраняет структуру uIcc: образ uIcc под castLE равен uIcc образов.
LaTeX
$$$\\mathrm{Fin}.\\mathrm{finsetImage}\\ (\\mathrm{castLE}\\ h)\\ (\\mathrm{Finset}.\\mathrm{uIcc}\\ a\\ b) = \\mathrm{Finset}.\\mathrm{uIcc}\\ (\\mathrm{Fin.castLE}\\ h\\ a) (\\mathrm{Fin.castLE}\\ h\\ b)$$$
Lean4
@[simp]
theorem finsetImage_castLE_uIcc (h : n ≤ m) : (uIcc a b).image (castLE h) = uIcc (castLE h a) (castLE h b) := by
simp [← coe_inj]