no goals
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
abv : β → α
inst✝¹ : Semiring β
inst✝ : IsAbsoluteValue abv
γ : Type u_1
f : γ → β
s : Finset γ
this : DecidableEq γ
⊢ abv (∑ k in ∅, f k) ≤ ∑ k in ∅, abv (f k)
simp [abv_zero abv]
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
abv : β → α
inst✝¹ : Semiring β
inst✝ : IsAbsoluteValue abv
γ : Type u_1
f : γ → β
s✝ : Finset γ
this : DecidableEq γ
a : γ
s : Finset γ
has : ¬a ∈ s
ih : abv (∑ k in s, f k) ≤ ∑ k in s, abv (f k)
⊢ abv (f a + ∑ x in s, f x) ≤ abv (f a) + ∑ x in s, abv (f x)
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
abv : β → α
inst✝¹ : Semiring β
inst✝ : IsAbsoluteValue abv
γ : Type u_1
f : γ → β
s✝ : Finset γ
this : DecidableEq γ
a : γ
s : Finset γ
has : ¬a ∈ s
ih : abv (∑ k in s, f k) ≤ ∑ k in s, abv (f k)
⊢ abv (∑ k in insert a s, f k) ≤ ∑ k in insert a s, abv (f k)
rw [sum_insert has, sum_insert has]
no goals
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
abv : β → α
inst✝¹ : Semiring β
inst✝ : IsAbsoluteValue abv
γ : Type u_1
f : γ → β
s✝ : Finset γ
this : DecidableEq γ
a : γ
s : Finset γ
has : ¬a ∈ s
ih : abv (∑ k in s, f k) ≤ ∑ k in s, abv (f k)
⊢ abv (f a + ∑ x in s, f x) ≤ abv (f a) + ∑ x in s, abv (f x)
exact le_trans (abv_add abv _ _) (add_le_add_left ih _)