Theorems · Theorem · order theory

biInf_inf

∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  (∃ i, p i) → (⨅ i, ⨅ (h : p i), f i h) ⊓ a = ⨅ i, ⨅ (h : p i), f i h ⊓ a

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CompleteLattice