erase_image_subset_image_erase — Mathlib

English

The image of s after erasing a is contained in the image of s after erasing a from the domain: (s.image f).erase (f a) ⊆ (s.erase a).image f.

Русский

Образ множества s после удаления элемента a через f содержится в образе s после удаления a из области: (s.image f).erase (f a) ⊆ (s.erase a).image f.

LaTeX

$$$(s.image f).erase (f a) \subseteq (s.erase a).image f$$$

Lean4

theorem erase_image_subset_image_erase [DecidableEq α] (f : α → β) (s : Finset α) (a : α) :
    (s.image f).erase (f a) ⊆ (s.erase a).image f := by grind

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