Theorems · Theorem · order theory

Set.image_image

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (s : Set α),
  g '' f '' s = (fun x => g (f x)) '' s

A variant of image_comp, useful for rewriting

Defined in

Mathlib.Data.Set.Image

Cited by

140 results in Mathlib

Foundations

Depth 9 from the axioms, rests on 23 definitions · uses propext, Quot.sound