finsetImage_castLE_Ioc — Mathlib

English

Casting preserves the half-open interval in the embedded nat range.

Русский

Преобразование сохраняет полуоткрытый интервал в встраиваемом натуральном диапазоне.

LaTeX

$$$(Ioc\ a\ b).\mathrm{image}(\mathrm{castLE}\ h) = Ioc(\mathrm{castLE}\ h\ a)(\mathrm{castLE}\ h\ b)$$

Lean4

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

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