Mathlib Map

Theorems · Theorem · order theory

IsGreatest.isLUB

∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → IsLUB s a
Defined in
Mathlib.Order.Bounds.Basic
Cited by
25 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isLUB_singleton · cited by 10isLUB_singletonIsGreatest.csSup_eq · cited by 9IsGreatest.csSup_eqnorm_cfc_le · cited by 3norm_cfc_lenorm_cfcₙ_le · cited by 3norm_cfcₙ_leisLUB_Iic · cited by 3isLUB_Iichimp_eq_sSup · cited by 2himp_eq_sSupisLUB_Icc · cited by 2isLUB_IccsSup_lowerBounds_eq_sInf · cited by 1sSup_lowerBounds_eq_sInfIsGreatest.upperBounds_eq · cited by 1IsGreatest.upperBounds_eqAEMeasurable.isLUB · cited by 1AEMeasurable.isLUBcsSup_lowerBounds_eq_csInf · cited by 1csSup_lowerBounds_eq_csInfnnnorm_cfcₙ_nnreal_le · cited by 1nnnorm_cfcₙ_nnreal_leisLUB_lowerBounds · cited by 1isLUB_lowerBoundscompl_eq_sSup_disjoint · cited by 1compl_eq_sSup_disjointisLUB_univ · cited by 1isLUB_univSet · cited by 53352SetPreorder · cited by 7952PreorderIsLUB · cited by 280IsLUBupperBounds · cited by 263upperBoundsIsGreatest · cited by 112IsGreatestIsGreatest.isLUBCITED BYCITES

Cites5

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
  • Preorderstatement and proof · cited by 7,952
  • IsLUBstatement · cited by 280
  • upperBoundsproof · cited by 263
  • IsGreateststatement and proof · cited by 112

Cited by25

Results whose statement or proof uses this declaration.