Theorems · Theorem · order theory
top_ne_bot
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [Nontrivial α], ⊤ ≠ ⊥- Defined in
- Mathlib.Order.BoundedOrder.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement and proof · cited by 9,680
- PartialOrderstatement and proof · cited by 6,410
- Bot.botstatement and proof · cited by 4,720
- Nontrivialstatement and proof · cited by 2,416
- BoundedOrderstatement and proof · cited by 270
- not_subsingletonproof · cited by 24
- subsingleton_of_top_eq_botproof · cited by 3
Cited by15
Results whose statement or proof uses this declaration.
- Submodule.top_ne_ideal_smul_of_le_jacobson_annihilatorproof · cited by 6
- isAtom_topproof · cited by 5
- IsLocalRing.ringJacobson_eq_maximalIdealproof · cited by 4
- Ideal.height_botproof · cited by 4
- Group.IsSolvable.commutator_lt_top_of_nontrivialproof · cited by 3
- LightProfinite.epi_iff_surjectiveproof · cited by 3
- Profinite.epi_iff_surjectiveproof · cited by 2
- ne_hnot_selfproof · cited by 2
- Set.Intersecting.is_max_iff_card_eqproof · cited by 2
- Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mulproof · cited by 2
- sSup_ne_topproof · cited by 1
- iSup_ne_topproof · cited by 1