map_castLEEmb_Ioc — Mathlib

English

For a,b ∈ Fin n and h with n ≤ m, the image of the half-open interval Ioc(a,b) under castLEEmb h is the half-open interval between castLE h a and castLE h b: map(Ioc(a,b)) = Ioc(castLE h a, castLE h b).

Русский

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

LaTeX

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

Lean4

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

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