Theorems · Theorem · order theory
ciSup_mono
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
BddAbove (Set.range g) → (∀ (x : ι), f x ≤ g x) → iSup f ≤ iSup gThe indexed suprema of two functions are comparable if the functions are pointwise comparable
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ConditionallyCompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.rangestatement and proof · cited by 4,705
- iSupstatement and proof · cited by 2,415
- le_reflproof · cited by 2,061
- SupSet.sSupproof · cited by 954
- IsEmptyproof · cited by 759
- BddAbovestatement and proof · cited by 620
- ConditionallyCompleteLatticestatement and proof · cited by 364
- isEmpty_or_nonemptyproof · cited by 269
- ciSup_leproof · cited by 56
- le_ciSup_of_leproof · cited by 22
- iSup_of_empty'proof · cited by 16
Cited by9
Results whose statement or proof uses this declaration.
- Cardinal.preBeth_limitproof · cited by 5
- ciSup_sup_eqproof · cited by 3
- ciSup_partialSups_eqproof · cited by 2
- Cardinal.ciSup_addproof · cited by 2
- Cardinal.ciSup_mulproof · cited by 2
- ciInf_monoproof · cited by 2
- CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eqproof · cited by 1
- Order.krullDim_eq_iSup_height_add_coheight_of_nonemptyproof · cited by 0
- Finite.ciSup_monoproof · cited by 0