Theorems · Theorem · order theory

Set.biUnion_and

∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι → Prop) (q : ι → ι' → Prop)
  (s : (x : ι) → (y : ι') → p x ∧ q x y → Set α),
  ⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯

Defined in

Mathlib.Data.Set.Lattice

Cited by

0 results in Mathlib

Foundations

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