Theorems · Theorem · order theory
lt_iff_le_and_ne
∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a < b ↔ a ≤ b ∧ a ≠ b- Defined in
- Mathlib.Order.Basic
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- le_of_ltproof · cited by 1,175
- ne_of_ltproof · cited by 203
- LE.le.lt_of_neproof · cited by 116
Cited by47
Results whose statement or proof uses this declaration.
- Order.IsSuccPrelimit.succ_ltproof · cited by 7
- wellFoundedGT_iff_monotone_chain_conditionproof · cited by 6
- SetLike.coe_ssubset_coeproof · cited by 5
- Set.ssubset_iff_subset_neproof · cited by 5
- RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonemptyproof · cited by 4
- Cardinal.add_le_add_iff_of_lt_aleph0proof · cited by 4
- LieAlgebra.InvariantForm.orthogonal_disjointproof · cited by 3
- AddLECancellable.lt_add_of_tsub_lt_leftproof · cited by 3
- Complex.neg_pi_div_two_lt_arg_iffproof · cited by 2
- ENNReal.HolderConjugate.lt_top_iff_one_ltproof · cited by 2
- Nat.not_prime_iff_minFac_ltproof · cited by 2
- MonomialOrder.eq_C_of_degree_eq_zeroproof · cited by 2