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}
[SeminormedAddCommGroup E]
{s : Set α}
(f : α → E)
(a : α)
: