image_preimage_of_bij — Mathlib

English

If f is bijective between s and its image, then the image of the preimage is exactly s.

Русский

Если f образует биекцию между s и его изображением, то образ предобраза равен ровно s.

LaTeX

$$$$ \\mathrm{image}(f)(\\mathrm{preimage}(s,f,hf.injOn)) = s. $$$$

Lean4

theorem image_preimage_of_bij [DecidableEq β] (f : α → β) (s : Finset β) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) :
    image f (preimage s f hf.injOn) = s :=
  Finset.coe_inj.1 <| by simpa using hf.image_eq

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