English
For any Fin n and m, the image of the open interval Ioo i j under castAdd m is Ioo (castAdd m i) (castAdd m j).
Русский
Для любых i, j ∈ Fin n и m ∈ ℕ образ Ioo i j под castAdd m равен Ioo (castAdd m i) (castAdd m j).
LaTeX
$$$ (\mathrm{Finset}.Ioo\, i\, j).image (\mathrm{Fin.castAdd}\, m) = \mathrm{Finset}.Ioo\ (\mathrm{Fin.castAdd}\, m\, i)\ (\mathrm{Fin.castAdd}\, m\, j) $$$
Lean4
@[simp]
theorem finsetImage_castAdd_Ioo (m) (i j : Fin n) : (Ioo i j).image (castAdd m) = Ioo (castAdd m i) (castAdd m j) :=
finsetImage_castLE_Ioo ..