Theorems · Theorem · order theory

ciSup_eq_ite

∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {p : Prop} [inst_1 : Decidable p] {f : p → α},
  ⨆ (h : p), f h = if h : p then f h else sSup ∅

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Cited by

4 results in Mathlib

Foundations

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

Assumes

ConditionallyCompletePartialOrderSupDecidable