Mathlib Map

Theorems · Theorem · order theory

mem_lowerBounds

∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x
Defined in
Mathlib.Order.Bounds.Basic
Cited by
19 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isGLB_lt_iff · cited by 6isGLB_lt_iffisGLB_image2_of_isGLB_isGLB · cited by 5isGLB_image2_of_isGLB_isG…AddSubgroup.exists_isLeast_pos · cited by 2AddSubgroup.exists_isLeas…Sion.minimax · cited by 2Sion.minimaxMeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range · cited by 2Martingale.bddAbove_range…IsGLB.biUnion_Ici_eq_Ici · cited by 2IsGLB.biUnion_Ici_eq_IciFinset.isGLB_iff_isLeast · cited by 2Finset.isGLB_iff_isLeastisLeast_univ_iff · cited by 2isLeast_univ_ifflimsup_const_sub · cited by 1limsup_const_subgc_lowerBounds_upperBounds · cited by 1gc_lowerBounds_upperBoundsLinearLocallyFiniteOrder.le_succFn · cited by 1LinearLocallyFiniteOrder.…exists_lub_Iio · cited by 1exists_lub_IioContinuous.exists_forall_le_of_hasCompactMulSupport · cited by 1Continuous.exists_forall_…Continuous.exists_forall_le_of_hasCompactSupport · cited by 1Continuous.exists_forall_…limsup_sub_const · cited by 0limsup_sub_constSet · cited by 53352SetPreorder · cited by 7952PreorderlowerBounds · cited by 212lowerBoundsmem_lowerBoundsCITED BYCITES

Cites3

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
  • lowerBoundsstatement · cited by 212

Cited by19

Results whose statement or proof uses this declaration.