α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
⊢ (if a ∈ s then f a else 0) ≤ f a
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (indicator s f)
refine' NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) _) hf
case inl
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : a ∈ s
⊢ f a ≤ f a

case inr
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : ¬a ∈ s
⊢ 0 ≤ f a
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
⊢ (if a ∈ s then f a else 0) ≤ f a
split_ifs
case inr
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : ¬a ∈ s
⊢ 0 ≤ f a
case inl
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : a ∈ s
⊢ f a ≤ f a

case inr
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : ¬a ∈ s
⊢ 0 ≤ f a
exact le_refl (f a)
no goals
case inr
α : Type u_1
β : Type ?u.317811
γ : Type ?u.317814
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : ¬a ∈ s
⊢ 0 ≤ f a
exact zero_le_coe