image_eq_preimage — Mathlib

English

Let f: α → α be an involution (f ∘ f = id). Then for every subset S ⊆ α, the image of S under f equals the preimage of S under f: f[S] = f^{-1}[S].

Русский

Пусть f: α → α является инволюцией (f ∘ f = id). Тогда для любого S ⊆ α выполняется f[S] = f^{-1}[S].

LaTeX

$$$$ \forall S \subseteq \alpha,\ f[S] = f^{-1}[S]. $$$$

Lean4

theorem _root_.Function.Involutive.image_eq_preimage {f : α → α} (hf : f.Involutive) : image f = preimage f :=
  image_eq_preimage_of_inverse hf.leftInverse hf.rightInverse

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