Theorems · Theorem · order theory

iInf_eq_dif

∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst_1 : Decidable p] (a : p → α),
  ⨅ (h : p), a h = if h : p then a h else ⊤

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLatticeDecidable