Theorems · Inductive type · order theory
OrderedSub
(α : Type u_2) → [LE α] → [Add α] → [Sub α] → Prop
OrderedSub α means that α has a subtraction characterized by a - b ≤ c ↔ a ≤ c + b.
In other words, a - b is the least c such that a ≤ b + c.
This is satisfied both by the subtraction in additive ordered groups and by truncated subtraction
in canonically ordered monoids on many specific types.
- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 236 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 4 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by239
Results whose statement or proof uses this declaration.
- add_tsub_cancel_rightstatement and proof · cited by 172
- tsub_selfstatement and proof · cited by 154
- tsub_zerostatement and proof · cited by 123
- tsub_add_cancel_of_lestatement and proof · cited by 112
- zero_tsubstatement and proof · cited by 100
- add_tsub_cancel_of_lestatement and proof · cited by 79
- tsub_le_iff_rightstatement and proof · cited by 49
- add_tsub_cancel_leftstatement and proof · cited by 42
- tsub_le_iff_leftstatement and proof · cited by 38
- tsub_eq_zero_iff_lestatement and proof · cited by 32
- tsub_pos_of_ltstatement and proof · cited by 31
- tsub_pos_iff_ltstatement and proof · cited by 27
Showing the 200 most cited of 239.