Mathlib Map

Theorems · Theorem · order theory

isTop_top

∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α], IsTop ⊤
Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
10 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
LEOrderTop
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isMax_top · cited by 12isMax_topSet.Iic_top · cited by 10Set.Iic_topFilter.OrderTop.atTop_eq · cited by 4OrderTop.atTop_eqOrder.cof_eq_one · cited by 2Order.cof_eq_oneisGreatest_univ · cited by 2isGreatest_univtendsto_rightLim_atTop_of_tendsto · cited by 2tendsto_rightLim_atTop_of…isGLB_empty · cited by 1isGLB_emptyStieltjesFunction.measure_Ici · cited by 1StieltjesFunction.measure…IsTop.rec · cited by 1IsTop.recSet.Ioi_eq_singleton_iff · cited by 0Set.Ioi_eq_singleton_iffSummationFilter.conditional_filter_eq_map_Ici · cited by 0SummationFilter.condition…Top.top · cited by 9680Top.topOrderTop · cited by 493OrderTople_top · cited by 411le_topIsTop · cited by 77IsTopisTop_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
  • OrderTopstatement and proof · cited by 493
  • le_topproof · cited by 411
  • IsTopstatement · cited by 77

Cited by11

Results whose statement or proof uses this declaration.