Mathlib Map

Theorems · Theorem · order theory

le_of_eq

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b → a ≤ b
Defined in
Mathlib.Order.Defs.PartialOrder
Cited by
366 results in Mathlib
Foundations
Depth 5 from the axioms, rests on 8 definitions · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Eq.le · cited by 605Eq.leContinuous.measurable · cited by 181Continuous.measurableIsFractionRing.injective · cited by 70IsFractionRing.injectivele_antisymm_iff · cited by 62le_antisymm_iffFilter.EventuallyEq.le · cited by 46EventuallyEq.leMeasureTheory.lintegral_mono_ae · cited by 36MeasureTheory.lintegral_m…Metric.sphere_subset_closedBall · cited by 24Metric.sphere_subset_clos…Filter.tendsto_add_atTop_nat · cited by 19Filter.tendsto_add_atTop_…MeasureTheory.lintegral_iSup · cited by 16MeasureTheory.lintegral_i…IsLocalRing.maximalIdeal_le_jacobson · cited by 16IsLocalRing.maximalIdeal_…MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff · cited by 14MeromorphicNFAt.meromorph…Multiset.card_eq_zero · cited by 13Multiset.card_eq_zeroAlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac · cited by 13IsOpenImmersion.isoOfRang…AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac · cited by 12IsOpenImmersion.isoOfRang…Ideal.map_isPrime_of_surjective · cited by 11Ideal.map_isPrime_of_surj…Preorder · cited by 7952Preorderle_refl · cited by 2061le_reflle_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 by366

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 366.