image_image — Mathlib

English

For a finite set s and functions f: α → β, g: β → γ, the result of first mapping by f and then by g equals mapping by the composition g ∘ f on s: (image g)(image f s) = image (g ∘ f) s.

Русский

Пусть s — конечное множество; функции f: α → β и g: β → γ. Образ сначала по f, затем по g равен образу по композиции g ∘ f: (image g)(image f s) = image (g ∘ f) s.

LaTeX

$$$(\mathrm{image}\ g)(\mathrm{image}\ f\ s) = \mathrm{image}\ (g \circ f)\ s$$$

Lean4

theorem image_image [DecidableEq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f) :=
  eq_of_veq <| by simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]

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