finsetImage_castLE_uIcc — Mathlib

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]

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