English
Let i, j ∈ Fin(m) and h with m ≤ n. Then the preimage of the interval uIcc(castLE(h i), castLE(h j)) under castLE(h) equals uIcc(i, j).
Русский
Пусть i, j ∈ Fin(m) и h с m ≤ n. Тогда предобраз интервала uIcc(castLE(h i), castLE(h j)) по отображению castLE(h) равен uIcc(i, j).
LaTeX
$$$castLE(h)^{-1}'\mathrm{uIcc}(\mathrm{castLE}(h,i), \mathrm{castLE}(h,j)) = \mathrm{uIcc}(i, j)$$$
Lean4
@[simp]
theorem preimage_castLE_uIcc_castLE (i j : Fin m) (h : m ≤ n) :
castLE h ⁻¹' uIcc (castLE h i) (castLE h j) = uIcc i j :=
rfl