image_eq_preimage_of_inverse — Mathlib

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)

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