Mathlib Map

Theorems · Theorem · order theory

le_of_forall_ge

∀ {α : Type u_2} [inst : Preorder α] {a b : α}, (∀ (c : α), a ≤ c → b ≤ c) → b ≤ a
Defined in
Mathlib.Order.Basic
Cited by
4 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Metric.hausdorffEDist_prod_le · cited by 4Metric.hausdorffEDist_pro…forall_ge_iff_le · cited by 0forall_ge_iff_leModuleCat.injectiveDimension_le_injectiveDimension_of_isLocalizedModule · cited by 0ModuleCat.injectiveDimens…ModuleCat.projectiveDimension_le_projectiveDimension_of_isLocalizedModule · cited by 0ModuleCat.projectiveDimen…Preorder · cited by 7952Preorderle_rfl · cited by 1558le_rflle_of_forall_geCITED BYCITES

Cites2

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
  • le_rflproof · cited by 1,558

Cited by4

Results whose statement or proof uses this declaration.