Mathlib Map

Theorems · Theorem · order theory

le_of_sub_nonneg

∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ a - b → b ≤ a

Alias of the forward direction of sub_nonneg.

Defined in
Mathlib.Algebra.Order.Group.Unbundled.Basic
Cited by
5 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext
Assumes
AddGroupLEAddRightMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Zsqrtd.sqLe_mul · cited by 1Zsqrtd.sqLe_mulnorm_eq_iInf_iff_real_inner_le_zero · cited by 1norm_eq_iInf_iff_real_inn…CHSH_inequality_of_comm · cited by 0CHSH_inequality_of_commpow_le_descPochhammer_eval · cited by 0pow_le_descPochhammer_evaltsirelson_inequality · cited by 0tsirelson_inequalityAddGroup · cited by 4410AddGroupAddRightMono · cited by 367AddRightMonosub_nonneg · cited by 167sub_nonnegle_of_sub_nonnegCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.