Mathlib Map

Theorems · Theorem · order theory

IsMin.not_isMax

∀ {β : Type u_2} [inst : PartialOrder β] [Nontrivial β] [IsCodirectedOrder β] {b : β}, IsMin b → ¬IsMax b
Defined in
Mathlib.Order.Directed
Cited by
2 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PartialOrderNontrivialIsCodirectedOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsMin.not_isMax' · cited by 0IsMin.not_isMax'Order.not_isMax_pred · cited by 0Order.not_isMax_predPartialOrder · cited by 6410PartialOrderNontrivial · cited by 2416NontrivialIsMax · cited by 372IsMaxIsMin · cited by 277IsMinLE.le.antisymm' · cited by 104le.antisymm'IsCodirectedOrder · cited by 95IsCodirectedOrderIsMax.not_lt · cited by 8IsMax.not_ltIsMin.isBot · cited by 4IsMin.isBotexists_lt_of_directed_ge · cited by 1exists_lt_of_directed_geIsMin.not_isMaxCITED BYCITES

Cites9

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.