map_castLEEmb_uIcc — Mathlib

English

For Fin n, Fin m with a, b : Fin n and h: n ≤ m, the image of uIcc a b under castLE h equals uIcc of castLE h a and castLE h b.

Русский

Для Fin n, Fin m с a, b: Fin n и h: n ≤ m, образ uIcc a b под castLE h равен uIcc castLE h a castLE h b.

LaTeX

$$$\\mathrm{Fin}.\\mathrm{map}\\ (\\mathrm{Fin.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 map_castLEEmb_uIcc (h : n ≤ m) : (uIcc a b).map (castLEEmb h) = uIcc (castLE h a) (castLE h b) := by
  simp [← coe_inj]

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