Mathlib Map

Theorems · Theorem · order theory

upperBounds_mono_set

∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → upperBounds t ⊆ upperBounds s
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.

BddAbove.mono · cited by 27BddAbove.monoMonotone.upperBounds_range_comp_tendsto_atTop · cited by 3Monotone.upperBounds_rang…IsLUB.mono · cited by 3IsLUB.monoIsLUB.of_isCofinalFor · cited by 2IsLUB.of_isCofinalForisLUB_iff_of_subset_of_subset_closure · cited by 2isLUB_iff_of_subset_of_su…IsGLB.of_subset_of_superset · cited by 1IsGLB.of_subset_of_supers…IsLUB.of_subset_of_superset · cited by 1IsLUB.of_subset_of_supers…upperBounds_supClosure · cited by 1upperBounds_supClosureMonotone.upperBounds_image_of_directedOn_prod · cited by 1Monotone.upperBounds_imag…upperBounds_countableSupClosure · cited by 1upperBounds_countableSupC…upperBounds_lowerClosure · cited by 1upperBounds_lowerClosureupperBounds_mono · cited by 1upperBounds_monounion_upperBounds_subset_upperBounds_inter · cited by 0union_upperBounds_subset_…Set · cited by 53352SetPreorder · cited by 7952PreorderupperBounds · cited by 263upperBoundsupperBounds_mono_setCITED 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
  • upperBoundsstatement and proof · cited by 263

Cited by13

Results whose statement or proof uses this declaration.