Mathlib Map

Theorems · Theorem · order theory

CovBy.lt

∀ {α : Type u_1} [inst : LT α] {a b : α}, a ⋖ b → a < b
Defined in
Mathlib.Order.Cover
Cited by
51 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
LT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsMin.isSuccPrelimit · cited by 5IsMin.isSuccPrelimitIsMax.isPredPrelimit · cited by 5IsMax.isPredPrelimitOrder.IsNormal.map_isSuccLimit · cited by 4IsNormal.map_isSuccLimitcsInf_mem_of_not_isPredLimit · cited by 3csInf_mem_of_not_isPredLi…Order.isSuccPrelimit_of_succ_lt · cited by 3Order.isSuccPrelimit_of_s…CovBy.Ico_eq · cited by 3CovBy.Ico_eqCovBy.Ioc_eq · cited by 3CovBy.Ioc_eqCovBy.Ioi_eq · cited by 3CovBy.Ioi_eqOrder.not_isPredPrelimit_iff_pred_eq · cited by 3Order.not_isPredPrelimit_…InitialSeg.isSuccPrelimit_apply_iff · cited by 3InitialSeg.isSuccPrelimit…Order.not_isSuccPrelimit_iff_succ_eq · cited by 3Order.not_isSuccPrelimit_…countable_setOfPred_covBy_right · cited by 3countable_setOfPred_covBy…csSup_mem_of_not_isSuccLimit · cited by 3csSup_mem_of_not_isSuccLi…CovBy.Iio_eq · cited by 2CovBy.Iio_eqIsLUB.isSuccPrelimit_of_notMem · cited by 2IsLUB.isSuccPrelimit_of_n…CovBy · cited by 290CovByCovBy.ltCITED BYCITES

Cites1

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

  • CovBystatement and proof · cited by 290

Cited by51

Results whose statement or proof uses this declaration.