Mathlib Map

Theorems · Theorem · order theory

IsMin.isBot

∀ {α : Type u_1} [inst : Preorder α] {a : α} [IsCodirectedOrder α], IsMin a → IsBot a
Defined in
Mathlib.Order.Directed
Cited by
4 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
PreorderIsCodirectedOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isBot_or_exists_lt · cited by 3isBot_or_exists_ltIsMin.not_isMax · cited by 2IsMin.not_isMaxFlag.isMin_coe · cited by 0Flag.isMin_coeisBot_iff_isMin · cited by 0isBot_iff_isMinPreorder · cited by 7952PreorderIsMin · cited by 277IsMinLE.le.trans' · cited by 140le.trans'IsCodirectedOrder · cited by 95IsCodirectedOrderIsBot · cited by 77IsBotexists_le_le · cited by 9exists_le_leIsMin.isBotCITED BYCITES

Cites6

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

Cited by4

Results whose statement or proof uses this declaration.