image_preimage — Mathlib

English

The image of the preimage equals the portion of s that lies in the range of f.

Русский

Образ предобраза равен той части s, которая лежит в области образа f.

LaTeX

$$$$ \\mathrm{image}(f)(\\mathrm{preimage}(s,f,hf)) = \\{x \\in s : x \\in \\mathrm{Range}(f)\\}. $$$$

Lean4

theorem image_preimage [DecidableEq β] (f : α → β) (s : Finset β) [∀ x, Decidable (x ∈ Set.range f)]
    (hf : Set.InjOn f (f ⁻¹' ↑s)) : image f (preimage s f hf) = {x ∈ s | x ∈ Set.range f} :=
  Finset.coe_inj.1 <| by
    simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range, ← Set.sep_mem_eq]; rfl

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