image_cast — Mathlib

English

If m = n, Fin.cast h is a bijection between Fin m and Fin n, hence for any subset s ⊆ Fin m we have Fin.cast h '' s = Fin.cast h.symm ⁻¹' s.

Русский

Если m = n, то Fin.cast h образует биекцию между Fin m и Fin n; для любого множества s ⊆ Fin m имеет место равенство Fin.cast h '' s = Fin.cast h.symm ⁻¹' s.

LaTeX

$$$$\\mathrm{Fin.cast}\\, h \\'' s = \\mathrm{Fin.cast}\\, h^{-1} \\!\\' s,$$$$

Lean4

theorem image_cast (h : m = n) (s : Set (Fin m)) : Fin.cast h '' s = Fin.cast h.symm ⁻¹' s :=
  (finCongr h).image_eq_preimage _

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