preimage_map — Mathlib

English

Mapping of a finite set and then taking preimage recovers the original set: preimage under the embedding of the mapped set equals the original.

Русский

Пусть s — множество, отображение f — вложение. Затем при взятии отображения и предобраза получаем исходное множество.

LaTeX

$$$$ (\\mathrm{preimage}(\\mathrm{map}\, f\, s, f, f.iso.injOn)) = s. $$$$

Lean4

@[simp]
theorem preimage_map (f : α ↪ β) (s : Finset α) : (s.map f).preimage f f.injective.injOn = s :=
  coe_injective <| by simp only [coe_preimage, coe_map, Set.preimage_image_eq _ f.injective]

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