intro g
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
⊢ Bounded f (max |boundᵤ| |boundₗ|)
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ |f g| ≤ max |boundᵤ| |boundₗ|