Theorems · Theorem · order theory

iInf_dite

∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α),
  (⨅ 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.Order.CompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLatticeDecidablePred