Mathlib Map

Theorems · Theorem · order theory

CovBy.wcovBy

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

Around this declaration

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

CovBy.Ioo_eq · cited by 6CovBy.Ioo_eqCovBy.ge_of_gt · cited by 6CovBy.ge_of_gtCovBy.le_of_lt · cited by 5CovBy.le_of_ltwcovBy_iff_covBy_or_le_and_le · cited by 3wcovBy_iff_covBy_or_le_an…CovBy.eq_or_eq · cited by 2CovBy.eq_or_eqCovBy.image · cited by 1CovBy.imageOrder.pred_eq_of_covBy · cited by 1Order.pred_eq_of_covByOrder.succ_eq_of_covBy · cited by 1Order.succ_eq_of_covByProd.mk_covBy_mk_iff · cited by 1Prod.mk_covBy_mk_iffcovBy_iff_wcovBy_and_lt · cited by 1covBy_iff_wcovBy_and_ltPi.covBy_iff_antisymmRel · cited by 0Pi.covBy_iff_antisymmRelModule.Basis.flag_wcovBy · cited by 0Basis.flag_wcovBycovBy_iff_wcovBy_and_ne · cited by 0covBy_iff_wcovBy_and_necovBy_iff_wcovBy_and_not_le · cited by 0covBy_iff_wcovBy_and_not_…CovBy.Icc_eq · cited by 0CovBy.Icc_eqPreorder · cited by 7952PreorderCovBy · cited by 290CovByWCovBy · cited by 107WCovByCovBy.le · cited by 10CovBy.leCovBy.wcovByCITED BYCITES

Cites4

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

  • Preorderstatement and proof · cited by 7,952
  • CovBystatement and proof · cited by 290
  • WCovBystatement · cited by 107
  • CovBy.leproof · cited by 10

Cited by15

Results whose statement or proof uses this declaration.