Mathlib Map

Theorems · Theorem · order theory

ge_of_eq

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → b ≤ a
Defined in
Mathlib.Order.Defs.PartialOrder
Cited by
67 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.

Eq.ge · cited by 375Eq.geLocalization.localRingHom_mk' · cited by 11Localization.localRingHom…ge_antisymm_iff · cited by 8ge_antisymm_iffsubsingleton_of_bot_eq_top · cited by 8subsingleton_of_bot_eq_topMeasureTheory.lintegral_eq_nnreal · cited by 6MeasureTheory.lintegral_e…isLeast_singleton · cited by 5isLeast_singletonMeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ · cited by 4MeasureTheory.ae_eq_of_fo…IsLocalHomeomorph.isOpenMap · cited by 4IsLocalHomeomorph.isOpenM…expNegInvGlue.nonneg · cited by 4expNegInvGlue.nonnegLinearMap.map_injective · cited by 4LinearMap.map_injectivene_of_not_ge · cited by 3ne_of_not_geOrder.pred_le_iff_eq_or_le · cited by 3Order.pred_le_iff_eq_or_leRingHom.surjective_localRingHom_iff · cited by 3RingHom.surjective_localR…Localization.localRingHom_mk · cited by 3Localization.localRingHom…Finset.eq_iff_card_le_of_subset · cited by 2Finset.eq_iff_card_le_of_…Preorder · cited by 7952Preorderle_refl · cited by 2061le_reflge_of_eqCITED 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_reflproof · cited by 2,061

Cited by67

Results whose statement or proof uses this declaration.