Mathlib Map

Theorems · Theorem · order theory

IsLeast.isGLB

∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → IsGLB s a
Defined in
Mathlib.Order.Bounds.Basic
Cited by
23 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.

IsLeast.csInf_eq · cited by 11IsLeast.csInf_eqisGLB_singleton · cited by 7isGLB_singletonisGLB_Ici · cited by 3isGLB_IciisGLB_Icc · cited by 2isGLB_IccsInf_upperBounds_eq_sSup · cited by 2sInf_upperBounds_eq_sSupFinset.le_min'_iff · cited by 2Finset.le_min'_iffFinset.isGLB_iff_isLeast · cited by 2Finset.isGLB_iff_isLeastcsInf_upperBounds_eq_csSup · cited by 2csInf_upperBounds_eq_csSupsdiff_eq_sInf · cited by 1sdiff_eq_sInfisGLB_Ico · cited by 1isGLB_IcoIsLeast.lowerBounds_eq · cited by 1IsLeast.lowerBounds_eqIsLeast.union · cited by 1IsLeast.unionIsCompact.exists_isGLB · cited by 1IsCompact.exists_isGLBFinset.min'_lt_max' · cited by 1Finset.min'_lt_max'RightOrdContinuous.map_isLeast · cited by 1RightOrdContinuous.map_is…Set · cited by 53352SetPreorder · cited by 7952PreorderIsGLB · cited by 213IsGLBlowerBounds · cited by 212lowerBoundsIsLeast · cited by 122IsLeastIsLeast.isGLBCITED 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
  • IsGLBstatement · cited by 213
  • lowerBoundsproof · cited by 212
  • IsLeaststatement and proof · cited by 122

Cited by23

Results whose statement or proof uses this declaration.