map_castLEEmb_Icc — Mathlib

English

Let a,b ∈ Fin n and h be such that n ≤ m. Then mapping the closed interval Icc(a,b) along the embedding castLEEmb h yields the closed interval between castLE h a and castLE h b: map(Icc(a,b)) = Icc(castLE h a, castLE h b).

Русский

Пусть a,b ∈ Fin n и h так, что n ≤ m. Тогда отображение отображения Icc(a,b) по вложению castLEEmb h даёт Icc(castLE h a, castLE h b).

LaTeX

$$$\operatorname{Finset.map}(\operatorname{castLEEmb}(h))(\mathrm{Icc}(a,b)) = \mathrm{Icc}(\operatorname{castLE}(h)a, \operatorname{castLE}(h)b)$$$

Lean4

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

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