Mathlib Map

Theorems · Theorem · order theory

IsCoatom.ne_top

∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → a ≠ ⊤
Defined in
Mathlib.Order.Atoms
Cited by
2 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
PreorderOrderTop
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsCoatom.codisjoint_of_ne · cited by 2IsCoatom.codisjoint_of_neIsCoatom.ne_iff_eq_top · cited by 1IsCoatom.ne_iff_eq_topTop.top · cited by 9680Top.topPreorder · cited by 7952PreorderOrderTop · cited by 493OrderTopIsCoatom · cited by 114IsCoatomIsCoatom.ne_topCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Top.topstatement · cited by 9,680
  • Preorderstatement and proof · cited by 7,952
  • OrderTopstatement and proof · cited by 493
  • IsCoatomstatement and proof · cited by 114

Cited by2

Results whose statement or proof uses this declaration.