Theorems · Theorem · order theory

Set.piMap_image_pi

∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {f : (i : ι) → α i → β i},
  (∀ i ∉ s, Function.Surjective (f 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

5 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Classical.choice, Quot.sound