Theorems · Theorem · order theory
le_of_not_ge
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → b ≤ a- Defined in
- Mathlib.Order.Defs.LinearOrder
- Cited by
- 72 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- LinearOrder
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.
- LinearOrderstatement and proof · cited by 8,572
- le_totalproof · cited by 294
Cited by72
Results whose statement or proof uses this declaration.
- lt_of_not_geproof · cited by 374
- le_max_leftproof · cited by 215
- Nat.exists_infinite_primesproof · cited by 7
- eVariationOn.edist_leproof · cited by 7
- IntervalIntegrable.comp_add_rightproof · cited by 6
- padicNorm.nonarchimedeanproof · cited by 5
- pow_eq_pow_iff_modEqproof · cited by 5
- ENNReal.mul_rpow_eq_iteproof · cited by 5
- nsmul_eq_nsmul_iff_modEqproof · cited by 4
- IsCoveringMap.exists_path_liftsproof · cited by 4
- IsPrimitiveRoot.pow_injproof · cited by 4
- countable_image_lt_image_Ioi_withinproof · cited by 3