[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f✝ : α → E
a✝ : α
h : s ⊆ t
f : α → E
a : α
⊢ ‖indicator s f a‖ ≤ ‖indicator t f a‖
[PROOFSTEP]
simp only [norm_indicator_eq_indicator_norm]
[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f✝ : α → E
a✝ : α
h : s ⊆ t
f : α → E
a : α
⊢ indicator s (fun a => ‖f a‖) a ≤ indicator t (fun a => ‖f a‖) a
[PROOFSTEP]
exact indicator_le_indicator_of_subset ‹_› (fun _ => norm_nonneg _) _
[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ ‖indicator s f a‖ ≤ ‖f a‖
[PROOFSTEP]
rw [norm_indicator_eq_indicator_norm]
[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ indicator s (fun a => ‖f a‖) a ≤ ‖f a‖
[PROOFSTEP]
apply indicator_norm_le_norm_self
