Theorems · Theorem · order theory

Set.iInter_ite

∀ {α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [inst : DecidablePred p] (f g : ι → Set α),
  (⋂ i, if p i then f i else g i) = (⋂ i, ⋂ (_ : p i), f i) ∩ ⋂ i, ⋂ (_ : ¬p i), g i

Defined in

Mathlib.Data.Set.Lattice

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidablePred