finsetImage_castLE_Ioo — Mathlib

English

Casting maps the open interval to the corresponding open interval after embedding.

Русский

Преобразование отображает открытый интервал в соответствующий после вложения.

LaTeX

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

Lean4

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

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