English
For m,n with m = n, the image of Fin.cast h equals the preimage under Fin.cast h.symm, i.e., image (Fin.cast h) = preimage (Fin.cast h.symm).
Русский
Для m = n верна тождество image (Fin.cast h) = preimage (Fin.cast h.symm).
LaTeX
$$$$\\mathrm{image}(\\mathrm{Fin.cast}\\, h) = \\mathrm{preimage}(\\mathrm{Fin.cast}\\, h.{\\mathrm{symm}})$$$$
Lean4
@[simp]
theorem image_cast_fun (h : m = n) : image (Fin.cast h) = preimage (Fin.cast h.symm) :=
funext <| image_cast h