α : Type u_2
E : Type u_1
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ indicator s (fun a => ‖f a‖) a ≤ ‖f a‖
α : Type u_2
E : Type u_1
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ ‖indicator s f a‖ ≤ ‖f a‖
rw [norm_indicator_eq_indicator_norm]
no goals
α : Type u_2
E : Type u_1
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ indicator s (fun a => ‖f a‖) a ≤ ‖f a‖
apply indicator_norm_le_norm_self