Theorems · Theorem · order theory
eq_top_or_lt_top
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] (a : α), a = ⊤ ∨ a < ⊤- Defined in
- Mathlib.Order.BoundedOrder.Basic
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrderOrderTop
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- PartialOrderstatement and proof · cited by 6,410
- OrderTopstatement and proof · cited by 493
- le_topproof · cited by 411
- LE.le.eq_or_ltproof · cited by 220
Cited by24
Results whose statement or proof uses this declaration.
- MeasureTheory.measureReal_union_leproof · cited by 4
- ContinuousLinearMap.opENorm_le_boundproof · cited by 3
- Dynamics.coverMincard_mul_le_powproof · cited by 2
- Dynamics.le_coverMincard_imageproof · cited by 2
- Dynamics.coverMincard_closure_leproof · cited by 2
- Dynamics.netMaxcard_le_coverMincardproof · cited by 2
- Dynamics.coverMincard_image_leproof · cited by 2
- Dynamics.coverMincard_le_netMaxcardproof · cited by 2
- ENNReal.lintegral_Lp_add_leproof · cited by 1
- MeasureTheory.measureReal_le_measureReal_union_leftproof · cited by 1
- MeasureTheory.mul_meas_ge_le_integral_of_nonnegproof · cited by 1
- lp.norm_le_of_tendstoproof · cited by 1