Theorems · Definition
iSup
{α : Type u} → {ι : Sort v} → [SupSet α] → (ι → α) → αIndexed supremum
- Defined in
- Mathlib.Order.SetNotation
- Cited by
- 2,415 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 8 definitions · uses no axioms
- Assumes
- SupSet
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.rangeproof · cited by 4,705
- SupSet.sSupproof · cited by 954
- SupSetstatement and proof · cited by 154
Cited by2,579
Results whose statement or proof uses this declaration.
- Set.iUnionproof · cited by 2,483
- iSup_congr_Propstatement and proof · cited by 247
- le_iSupstatement · cited by 207
- iSup_lestatement · cited by 190
- Metric.ediamproof · cited by 159
- FormalMultilinearSeries.radiusproof · cited by 150
- iSupIndepproof · cited by 100
- iSup₂_lestatement · cited by 96
- eVariationOnproof · cited by 90
- Filter.codiscreteWithinproof · cited by 87
- Order.krullDimproof · cited by 82
- le_iSup_of_lestatement · cited by 79
Showing the 200 most cited of 2,579.