Theorems · Definition
Top.top
{α : Type u_1} → [self : Top α] → αThe top (⊤, \top) element
Conventions for notations in identifiers:
* The recommended spelling of ⊤ in identifiers is top.
- Defined in
- Mathlib.Order.Notation
- Cited by
- 9,680 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Top
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Topstatement and proof · cited by 93
Cited by10,674
Results whose statement or proof uses this declaration.
- LinearMap.rangeproof · cited by 893
- MeasureTheory.Lpproof · cited by 715
- MeasureTheory.MemLpproof · cited by 457
- le_topstatement · cited by 411
- ContDiffproof · cited by 352
- MeasureTheory.eLpNormproof · cited by 329
- MonoidHom.rangeproof · cited by 314
- ContDiffWithinAtproof · cited by 283
- eq_top_iffstatement · cited by 236
- Finset.infproof · cited by 219
- Codisjointproof · cited by 197
- top_le_iffstatement · cited by 175
Showing the 200 most cited of 10,674.