Theorems · Theorem · order theory
eq_of_le_of_ge
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = bAlias of le_antisymm.
- Defined in
- Mathlib.Order.Defs.PartialOrder
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement · cited by 6,410
- le_antisymmproof · cited by 2,068
Cited by16
Results whose statement or proof uses this declaration.
- PowerSeries.order_eq_orderproof · cited by 4
- MonotoneOn.eVariationOn_eqproof · cited by 4
- EReal.limsup_const_mul_of_nonneg_of_ne_topproof · cited by 3
- Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonnegproof · cited by 3
- SimpleGraph.isExtremal_free_iffproof · cited by 2
- MvPowerSeries.order_expandproof · cited by 1
- FormalMultilinearSeries.radius_shiftproof · cited by 1
- Polynomial.zero_le_eval_of_roots_le_of_leadingCoeff_nonnegproof · cited by 1
- PMF.support_bernoulliproof · cited by 1
- MvPowerSeries.order_toSubringproof · cited by 0
- FormalMultilinearSeries.radius_smul_eqproof · cited by 0
- SummationFilter.eq_unconditional_of_finiteproof · cited by 0