Mathlib Map

Theorems · Definition · order theory

IsGreatest

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

a is a greatest element of a set s; for a partial order, it is unique if exists.

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

Around this declaration

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

IsGLB · cited by 213IsGLBIsGreatest.isLUB · cited by 25IsGreatest.isLUBIsGreatest.csSup_eq · cited by 9IsGreatest.csSup_eqIsGreatest.norm_cfc · cited by 6IsGreatest.norm_cfcIsGreatest.unique · cited by 6IsGreatest.uniqueisGreatest_singleton · cited by 5isGreatest_singletonIsGreatest.nnnorm_cfc_nnreal · cited by 5IsGreatest.nnnorm_cfc_nnr…IsGreatest.nnnorm_cfcₙ_nnreal · cited by 5IsGreatest.nnnorm_cfcₙ_nn…IsGreatest.norm_cfcₙ · cited by 5IsGreatest.norm_cfcₙMonotoneOn.map_isGreatest · cited by 5MonotoneOn.map_isGreatestisGreatest_Icc · cited by 4isGreatest_IccisGreatest_Iic · cited by 4isGreatest_IicMonotone.map_isGreatest · cited by 4Monotone.map_isGreatesteVariationOn.union · cited by 4eVariationOn.unionsigPos_isGreatest · cited by 4sigPos_isGreatestSet · cited by 53352SetupperBounds · cited by 263upperBoundsIsGreatestCITED 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
  • upperBoundsproof · cited by 263

Cited by115

Results whose statement or proof uses this declaration.