image_sdiff_of_injOn — Mathlib

English

Let s and t be Finset α with t ⊆ s, and f: α → β. If f is injective on s, then (s \\ t).image f = s.image f \\ t.image f.

Русский

Пусть s и t — конечные множества (Finset) α, t ⊆ s, и f: α → β. При условии, что f инъективна на s, верно (s \\ t).image f = s.image f \\ t.image f.

LaTeX

$$$ (s \\setminus t).image f = s.image f \\setminus t.image f $$$

Lean4

theorem image_sdiff_of_injOn [DecidableEq α] {t : Finset α} (hf : Set.InjOn f s) (hts : t ⊆ s) :
    (s \ t).image f = s.image f \ t.image f :=
  mod_cast Set.image_diff_of_injOn hf <| coe_subset.2 hts

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