Mathlib Map

Theorems · Theorem · order theory

IsCofinal.top_mem

∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {s : Set α}, IsCofinal s → ⊤ ∈ s
Defined in
Mathlib.Order.Cofinal
Cited by
2 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
PartialOrderOrderTop
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsClub.sInter_of_orderTop · cited by 2IsClub.sInter_of_orderTopisCofinal_iff_top_mem · cited by 1isCofinal_iff_top_memSet · cited by 53352SetTop.top · cited by 9680Top.topPartialOrder · cited by 6410PartialOrderOrderTop · cited by 493OrderTopIsCofinal · cited by 84IsCofinalisMax_top · cited by 12isMax_topIsCofinal.mem_of_isMax · cited by 1IsCofinal.mem_of_isMaxIsCofinal.top_memCITED BYCITES

Cites7

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

Cited by2

Results whose statement or proof uses this declaration.