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