Indicator function and norm
This file contains a few simple lemmas about set.indicator and norm.
Tags
indicator, norm
theorem
nnnorm_indicator_eq_indicator_nnnorm
{α : Type u_1}
{E : Type u_2}
[normed_group E]
{s : set α}
(f : α → E)
(a : α) :
theorem
indicator_norm_le_norm_self
{α : Type u_1}
{E : Type u_2}
[normed_group E]
{s : set α}
(f : α → E)
(a : α) :
theorem
norm_indicator_le_norm_self
{α : Type u_1}
{E : Type u_2}
[normed_group E]
{s : set α}
(f : α → E)
(a : α) :