Theorems · Theorem · order theory
Monotone.map_bddBelow
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → ∀ {s : Set α}, BddBelow s → BddBelow (f '' s)The image under a monotone function of a set which is bounded below is bounded below.
See also BddBelow.image2.
- Defined in
- Mathlib.Order.Bounds.Image
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Set.imagestatement and proof · cited by 5,609
- Monotonestatement and proof · cited by 1,397
- BddBelowstatement and proof · cited by 401
- lowerBoundsproof · cited by 212
- Monotone.mem_lowerBounds_imageproof · cited by 11
Cited by7
Results whose statement or proof uses this declaration.
- BddBelow.range_comp_leftproof · cited by 3
- GaloisConnection.u_csInf_of_directedOn'proof · cited by 2
- WithTop.coe_sInf'proof · cited by 2
- Monotone.csInf_image_leproof · cited by 2
- GaloisConnection.bddBelow_u_imageproof · cited by 1
- Antitone.map_bddBelowproof · cited by 1
- BddBelow.smul_of_nonnegproof · cited by 0