Mathlib Map

Theorems · Theorem · order theory

IsTop.isMax

∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsMax a
Defined in
Mathlib.Order.Max
Cited by
7 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isMax_top · cited by 12isMax_topSet.subsingleton_isTop · cited by 5Set.subsingleton_isTopisTop_iff_eq_top · cited by 3isTop_iff_eq_topnhdsGT_eq_bot_iff · cited by 1nhdsGT_eq_bot_iffisTop_iff_isMax · cited by 1isTop_iff_isMaxSubsingleton.isMax · cited by 0Subsingleton.isMaxIsBot.not_isTop · cited by 0IsBot.not_isTopIsMax · cited by 372IsMaxIsTop · cited by 77IsTopIsTop.isMaxCITED BYCITES

Cites2

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

  • IsMaxstatement · cited by 372
  • IsTopstatement and proof · cited by 77

Cited by7

Results whose statement or proof uses this declaration.