Mathlib Map

Theorems · Theorem · order theory

mabs_sup_div_sup_le_mabs

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b c : α), |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ
Defined in
Mathlib.Algebra.Order.Group.Unbundled.Abs
Cited by
1 results in Mathlib
Foundations
Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LatticeCommGroupMulLeftMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

m_Birkhoff_inequalities · cited by 0m_Birkhoff_inequalitiesle_refl · cited by 2061le_reflCommGroup · cited by 990CommGroupLattice · cited by 916LatticeMulLeftMono · cited by 410MulLeftMonomabs · cited by 148mabsone_le_mabs · cited by 11one_le_mabsmabs_div_sup_mul_mabs_div_inf · cited by 2mabs_div_sup_mul_mabs_div…le_of_mul_le_of_one_le_left · cited by 1le_of_mul_le_of_one_le_le…mabs_sup_div_sup_le_mabsCITED BYCITES

Cites8

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

Cited by1

Results whose statement or proof uses this declaration.