Mathlib Map

Theorems · Theorem · order theory

min_neg_neg

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b : α),
  min (-a) (-b) = -max a b
Defined in
Mathlib.Algebra.Order.Group.MinMax
Cited by
4 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext, Quot.sound
Assumes
AddCommGroupLinearOrderIsOrderedAddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

padicValRat_two_harmonic · cited by 2padicValRat_two_harmonicFilter.comap_abs_atTop · cited by 2Filter.comap_abs_atTopmin_sub_sub_left · cited by 1min_sub_sub_leftSet.preimage_const_sub_uIcc · cited by 0Set.preimage_const_sub_uI…AddCommGroup · cited by 12871AddCommGroupLinearOrder · cited by 8572LinearOrderIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidneg_le_neg_iff · cited by 57neg_le_neg_iffMonotone.map_max · cited by 55Monotone.map_maxmin_neg_negCITED BYCITES

Cites5

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

Cited by4

Results whose statement or proof uses this declaration.