image_cast_fun — Mathlib

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

Похожие утверждения