Theorems · Theorem · order theory

Set.uncurry_preimage_sigma_pi

∀ {ι : Type u_1} {α : ι → Type u_3} {β : (i : ι) → α i → Type u_7} (s : Set ι) (t : (i : ι) → Set (α i))
  (u : (p : (i : ι) × α i) → Set (β p.fst p.snd)),
  Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi fun i => (t i).pi fun j => u ⟨i, j⟩

Defined in

Mathlib.Data.Set.Sigma

Cited by

1 results in Mathlib

Foundations

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