Mathlib Map

Theorems · Theorem · order theory

bddAbove_def

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

Around this declaration

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

Order.exists_series_of_le_height · cited by 4Order.exists_series_of_le…bddAbove_iff_exists_ge · cited by 3bddAbove_iff_exists_geNNReal.bddAbove_range_agmSequences_fst · cited by 3NNReal.bddAbove_range_agm…ConvexOn.sSup_of_countable_affine_eq · cited by 2ConvexOn.sSup_of_countabl…ciSup_prod · cited by 2ciSup_prodMeasureTheory.dist_convolution_le' · cited by 1MeasureTheory.dist_convol…Order.height_eq_top_iff · cited by 1Order.height_eq_top_iffConvexOn.univ_sSup_of_countable_affine_eq · cited by 1ConvexOn.univ_sSup_of_cou…Complex.HadamardThreeLines.F_BddAbove · cited by 1HadamardThreeLines.F_BddA…CauchySeq.norm_bddAbove · cited by 1CauchySeq.norm_bddAboveNorthcott.comp_of_bddAbove · cited by 0Northcott.comp_of_bddAboveCauchySeq.mul_norm_bddAbove · cited by 0CauchySeq.mul_norm_bddAbo…Matroid.existsMaximalSubsetProperty_of_bdd · cited by 0Matroid.existsMaximalSubs…Set · cited by 53352SetPreorder · cited by 7952PreorderBddAbove · cited by 620BddAbovebddAbove_defCITED 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
  • BddAbovestatement · cited by 620

Cited by13

Results whose statement or proof uses this declaration.