Theorems · Theorem · order theory
abs_abs_sub_abs_le
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), ||a| - |b|| ≤ |a - b|- Cited by
- 1 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- AddGroupproof · cited by 4,410
- absstatement and proof · cited by 1,814
- sub_eq_add_negproof · cited by 1,023
- neg_negproof · cited by 960
- Latticestatement and proof · cited by 916
- AddLeftMonostatement and proof · cited by 687
- sub_add_cancelproof · cited by 344
- neg_add_revproof · cited by 236
- sup_le_iffproof · cited by 58
- sub_le_iff_le_addproof · cited by 50
- abs_sub_commproof · cited by 40
Cited by1
Results whose statement or proof uses this declaration.
- norm_abs_sub_absproof · cited by 0