English
Let f: A → B and g: B → A be mutual inverses (g ∘ f = id_A and f ∘ g = id_B). Then for every subset S ⊆ A, the image of S under f equals the preimage of S under g, i.e. f[S] = g^{-1}[S].
Русский
Пусть f: A → B и g: B → A являются взаимно обратными (g ∘ f = id_A и f ∘ g = id_B). Тогда для любого подмножества S ⊆ A выполняется f[S] = g^{-1}[S].
LaTeX
$$$$ \forall S \subseteq A,\ f[S] = g^{-1}[S]. $$$$
Lean4
theorem image_eq_preimage_of_inverse {f : α → β} {g : β → α} (h₁ : LeftInverse g f) (h₂ : RightInverse g f) :
image f = preimage g :=
funext fun s => Subset.antisymm (image_subset_preimage_of_inverse h₁ s) (preimage_subset_image_of_inverse h₂ s)