Theorems · Theorem · order theory
lt_of_lt_of_le
∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c- Defined in
- Mathlib.Order.Defs.PartialOrder
- Cited by
- 438 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 11 definitions · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- le_of_ltproof · cited by 1,175
- le_transproof · cited by 985
- not_le_of_gtproof · cited by 97
- lt_of_le_not_geproof · cited by 33
Cited by438
Results whose statement or proof uses this declaration.
- LT.lt.trans_leproof · cited by 678
- Real.pi_posproof · cited by 173
- Real.exp_posproof · cited by 169
- lt_transproof · cited by 165
- Real.rpow_le_rpow_of_exponent_leproof · cited by 32
- le_of_forall_gt_imp_ge_of_denseproof · cited by 21
- Set.Iio_subset_Iioproof · cited by 18
- Metric.ball_subset_ballproof · cited by 18
- Filter.eventually_lt_of_lt_liminfproof · cited by 17
- Real.exp_strictMonoproof · cited by 17
- MeasureTheory.lintegral_iSupproof · cited by 16
- Metric.eball_subset_eballproof · cited by 14
Showing the 200 most cited of 438.