Theorems · Theorem · order theory

Set.piMap_image_pi_subset

∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {f : (i : ι) → α i → β i} (t : (i : ι) → Set (α i)),
  Pi.map f '' s.pi t ⊆ s.pi fun i => f i '' t i

Defined in

Mathlib.Data.Set.Prod

Cited by

3 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext, Quot.sound