Module docstring
{"# Some lemmas on extended non-negative reals
These are some lemmas split off from ENNReal.Basic because they need a lot more imports.
They are probably good targets for further cleanup or moves.
"}
ENNReal.coe_indicator
theorem
{α} (s : Set α) (f : α → ℝ≥0) (a : α) : ((s.indicator f a : ℝ≥0) : ℝ≥0∞) = s.indicator (fun x => ↑(f x)) a
Full source
@[simp, norm_cast]
theorem coe_indicator {α} (s : Set α) (f : α → ℝ≥0) (a : α) :
((s.indicator f a : ℝ≥0) : ℝ≥0∞) = s.indicator (fun x => ↑(f x)) a :=
(ofNNRealHom : ℝ≥0ℝ≥0 →+ ℝ≥0∞).map_indicator _ _ _Informal description
For any set $s$ over a type $\alpha$ and any function $f : \alpha \to \mathbb{R}_{\geq 0}$, the canonical inclusion of the indicator function of $s$ applied to $f$ at a point $a \in \alpha$ into the extended nonnegative reals equals the indicator function of $s$ applied to the composition of $f$ with the canonical inclusion into the extended nonnegative reals, evaluated at $a$.
In symbols, for any $a \in \alpha$:
$$ \overline{(s \text{.indicator } f \ a)} = s \text{.indicator } (\lambda x, \overline{f(x)}) \ a $$
where $\overline{\cdot}$ denotes the canonical inclusion $\mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.coe_finset_sup
theorem
{s : Finset α} {f : α → ℝ≥0} : ↑(s.sup f) = s.sup fun x => (f x : ℝ≥0∞)
Full source
@[simp, norm_cast]
theorem coe_finset_sup {s : Finset α} {f : α → ℝ≥0} : ↑(s.sup f) = s.sup fun x => (f x : ℝ≥0∞) :=
Finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rflInformal description
For any finite set $s$ and any function $f : \alpha \to \mathbb{R}_{\geq 0}$, the canonical inclusion of the supremum of $f$ over $s$ into the extended nonnegative reals equals the supremum over $s$ of the composition of $f$ with the canonical inclusion into the extended nonnegative reals.
In symbols:
$$ \overline{\sup_{x \in s} f(x)} = \sup_{x \in s} \overline{f(x)} $$
where $\overline{\cdot}$ denotes the canonical inclusion $\mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$.