Mathlib Map

Theorems · Definition · order theory

upperBounds

{α : Type u_1} → [LE α] → Set α → Set α

The set of upper bounds of a set.

Defined in
Mathlib.Order.Bounds.Defs
Cited by
263 results in Mathlib
Foundations
Depth 4 from the axioms, rests on 10 definitions · uses no axioms
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BddAbove · cited by 620BddAboveIsLUB · cited by 280IsLUBIsGreatest · cited by 112IsGreatestIsGreatest.isLUB · cited by 25IsGreatest.isLUBisLUB_le_iff · cited by 24isLUB_le_iffmem_upperBounds · cited by 20mem_upperBoundsOrdinal.bddAbove_of_small · cited by 19Ordinal.bddAbove_of_smallupperBounds_mono_set · cited by 13upperBounds_mono_setMonotone.mem_upperBounds_image · cited by 12Monotone.mem_upperBounds_…IsLUB.upperBounds_eq · cited by 10IsLUB.upperBounds_eqFirstOrder.Language.DirectLimit.unify · cited by 10DirectLimit.unifyMonotone.map_bddAbove · cited by 9Monotone.map_bddAbovecsSup_le' · cited by 8csSup_le'isLUB_Ioo · cited by 7isLUB_IooisLUB_of_tendsto_atTop · cited by 7isLUB_of_tendsto_atTopSet · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredupperBoundsCITED BYCITES

Cites2

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

  • Setstatement and proof · cited by 53,352
  • Set.ofPredproof · cited by 6,101

Cited by272

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 272.