Theorems · Theorem · order theory

Set.iInter_dite

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

Defined in

Mathlib.Data.Set.Lattice

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidablePred