image_image — Mathlib

English

The image of the image under g after f equals the image under the composition g ∘ f on the same set.

Русский

Образ образа функции f под g равен образу композиции g ∘ f на том же множестве.

LaTeX

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

Lean4

/-- A variant of `image_comp`, useful for rewriting -/
@[grind =]
theorem image_image (g : β → γ) (f : α → β) (s : Set α) : g '' (f '' s) = (fun x => g (f x)) '' s :=
  (image_comp g f s).symm

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