Theorems · Theorem · order theory

Set.biInter_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