Mathlib Map

Theorems · Theorem · order theory

lowerBounds_mono_set

∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → lowerBounds t ⊆ lowerBounds s
Defined in
Mathlib.Order.Bounds.Basic
Cited by
12 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.

BddBelow.mono · cited by 16BddBelow.monolowerBounds_infClosure · cited by 1lowerBounds_infClosureIsGLB.of_subset_of_superset · cited by 1IsGLB.of_subset_of_supers…exists_countable_upperSemicontinuous_isGLB · cited by 1exists_countable_upperSem…lowerBounds_upperClosure · cited by 1lowerBounds_upperClosureMonotone.lowerBounds_range_comp_tendsto_atBot · cited by 1Monotone.lowerBounds_rang…IsGLB.mono · cited by 1IsGLB.monolowerBounds_countableInfClosure · cited by 1lowerBounds_countableInfC…IsLUB.of_subset_of_superset · cited by 1IsLUB.of_subset_of_supers…lowerBounds_mono · cited by 0lowerBounds_monoIsGLB.of_isCoinitialFor · cited by 0IsGLB.of_isCoinitialForunion_lowerBounds_subset_lowerBounds_inter · cited by 0union_lowerBounds_subset_…Set · cited by 53352SetPreorder · cited by 7952PreorderlowerBounds · cited by 212lowerBoundslowerBounds_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
  • lowerBoundsstatement and proof · cited by 212

Cited by12

Results whose statement or proof uses this declaration.