English
Let m, n be natural numbers with m = n, and let i be an element of Fin n. Then the preimage of the interval Ici i under the cast map Fin.cast h is the interval Ici (i.cast h.symm).
Русский
Пусть m, n — натуральные числа и m = n, и пусть i ∈ Fin n. Тогда прообраз интервала Ici i по отображению Fin.cast h равен интервалу Ici (i.cast h.symm).
LaTeX
$$$ \operatorname{Set.preimage}(\operatorname{Fin.cast} h)\, (\operatorname{Set.Ici} i) = \operatorname{Ici}(i.cast\, h.symm) $$$
Lean4
@[simp]
theorem preimage_cast_Ici (h : m = n) (i : Fin n) : .cast h ⁻¹' Ici i = Ici (i.cast h.symm) :=
rfl