Theorems · Theorem · order theory
exists_between
∀ {α : Type u_2} [inst : LT α] [DenselyOrdered α] {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂- Defined in
- Mathlib.Order.Basic
- Cited by
- 102 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 5 definitions · uses no axioms
- Assumes
- LTDenselyOrdered
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.
- DenselyOrderedstatement and proof · cited by 471
- DenselyOrdered.denseproof · cited by 8
Cited by102
Results whose statement or proof uses this declaration.
- Set.nonempty_Iooproof · cited by 23
- le_of_forall_gt_imp_ge_of_denseproof · cited by 21
- isGLB_Iooproof · cited by 5
- hasFDerivAt_jacobiTheta₂proof · cited by 4
- Metric.mk_uniformity_basis_leproof · cited by 4
- LinearOrderedAddCommGroup.discrete_iff_not_denselyOrderedproof · cited by 4
- continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithinproof · cited by 4
- ENNReal.exists_pos_sum_of_countableproof · cited by 4
- StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioiproof · cited by 4
- StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iioproof · cited by 4
- image_le_of_liminf_slope_right_lt_deriv_boundary'proof · cited by 4
- exists_pos_lt_subset_ballproof · cited by 4