Theorems · Theorem · order theory
Ne.le_iff_lt
∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → (a ≤ b ↔ a < b)- Defined in
- Mathlib.Order.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- LT.lt.leproof · cited by 2,189
- lt_of_le_of_neproof · cited by 230
Cited by8
Results whose statement or proof uses this declaration.
- Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_memproof · cited by 3
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- Finset.offDiag_filter_lt_eq_filter_leproof · cited by 1
- sameRay_neg_smul_right_iff_of_neproof · cited by 1
- Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁'proof · cited by 1
- sameRay_smul_right_iff_of_neproof · cited by 1
- not_monotone_not_antitone_iff_exists_lt_ltproof · cited by 0
- AlgebraicTopology.DoldKan.HigherFacesVanish.inductionproof · cited by 0