image_rev — Mathlib

English

For any subset s of Fin(n), the image of s under the reversal map equals the preimage of s under the reversal map.

Русский

Для любого подмножества s Fin(n) образ под реверсом равен предобразу под реверсом.

LaTeX

$$$\mathrm{Set.image}(\mathrm{Fin.rev}, s) = \mathrm{Set.preimage}(\mathrm{Fin.rev}, s)$$$

Lean4

theorem image_rev (s : Set (Fin n)) : rev '' s = rev ⁻¹' s :=
  revPerm.image_eq_preimage s

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