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