Theorems · Inductive type
SupSet
Type u_1 → Type u_1
Class for the sSup operator
- Defined in
- Mathlib.Order.SetNotation
- Cited by
- 154 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by224
Results whose statement or proof uses this declaration.
- iSupstatement and proof · cited by 2,415
- SupSet.sSupstatement and proof · cited by 954
- iSup_congr_Propstatement and proof · cited by 247
- sSupHomstatement · cited by 40
- sSup_eq_iSup'statement and proof · cited by 38
- iSup_applystatement and proof · cited by 35
- sSup_rangestatement and proof · cited by 20
- MeasureTheory.lintegral_const_mulproof · cited by 19
- MeasureTheory.lintegral_mapproof · cited by 17
- iSup_of_empty'statement and proof · cited by 16
- iSup_congrstatement and proof · cited by 15
- Equiv.iSup_compstatement and proof · cited by 14
Showing the 200 most cited of 224.