Mathlib Map

Theorems · Theorem · order theory

IsMax.not_lt

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → ¬a < b
Defined in
Mathlib.Order.Max
Cited by
8 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

not_top_lt · cited by 17not_top_ltnot_isMax_of_lt · cited by 6not_isMax_of_ltSet.Ico_succ_left_eq_Ioo · cited by 4Set.Ico_succ_left_eq_Iooexists_subset_iUnion_closure_subset · cited by 3exists_subset_iUnion_clos…exists_subset_iUnion_closure_subset_t2space · cited by 2exists_subset_iUnion_clos…IsMin.not_isMax · cited by 2IsMin.not_isMaxisMax_iff_forall_not_lt · cited by 2isMax_iff_forall_not_ltPrimeSpectrum.isMax_iff · cited by 1PrimeSpectrum.isMax_iffPreorder · cited by 7952PreorderLT.lt.le · cited by 2189lt.leIsMax · cited by 372IsMaxLT.lt.not_ge · cited by 305lt.not_geIsMax.not_ltCITED BYCITES

Cites4

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

Cited by8

Results whose statement or proof uses this declaration.