Mathlib Map

Theorems · Theorem · order theory

sup_eq_maxDefault

∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : DecidableLE α] [Std.Total fun x1 x2 => x1 ≤ x2],
  (fun x1 x2 => x1 ⊔ x2) = maxDefault
Defined in
Mathlib.Order.Lattice
Cited by
4 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext, Quot.sound
Assumes
SemilatticeSupDecidableLEStd.Total
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

posPart_eq_ite · cited by 0posPart_eq_itenegPart_eq_ite · cited by 0negPart_eq_iteoneLePart_eq_ite · cited by 0oneLePart_eq_iteleOnePart_eq_ite · cited by 0leOnePart_eq_iteSemilatticeSup · cited by 785SemilatticeSupsup_of_le_left · cited by 218sup_of_le_leftsup_of_le_right · cited by 143sup_of_le_righttotal_of · cited by 11total_ofmaxDefault · cited by 1maxDefaultsup_eq_maxDefaultCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.