Theorems · Theorem · order theory
BddAbove.mono
∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddAbove t → BddAbove sIf s ⊆ t and t is bounded above, then so is s.
- Defined in
- Mathlib.Order.Bounds.Basic
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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
- BddAbovestatement · cited by 620
- Set.Nonempty.monoproof · cited by 88
- upperBounds_mono_setproof · cited by 13
Cited by27
Results whose statement or proof uses this declaration.
- Ordinal.log_of_left_le_oneproof · cited by 13
- Monotone.ciSup_comp_tendsto_atTopproof · cited by 4
- ciSup_subtypeproof · cited by 4
- le_ciSup₂proof · cited by 3
- ConvexOn.locallyLipschitzOnproof · cited by 3
- ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interiorproof · cited by 2
- Dense.ciSupproof · cited by 2
- MonotoneOn.exists_monotone_extensionproof · cited by 2
- Complex.HadamardThreeLines.scale_bddAboveproof · cited by 2
- zero_memℓpproof · cited by 1
- Order.IsNormal.iSup_iterate_mem_fixedPointsproof · cited by 1
- Dense.ciSup'proof · cited by 1