map_castLEEmb_Ioo — Mathlib

English

Let a,b ∈ Fin n and h with n ≤ m. Then the image under castAddEmb h of the open interval Ioo(a,b) is the open interval Ioo between castAdd h a and castAdd h b: map(Ioo(a,b)) = Ioo(castAdd h a, castAdd h b).

Русский

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

LaTeX

$$$\operatorname{Finset.map}(\operatorname{castAddEmb}(h))(\mathrm{Ioo}(a,b)) = \mathrm{Ioo}(\operatorname{castAdd}(h)a, \operatorname{castAdd}(h)b)$$$

Lean4

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

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