English
A multiset of functions, each strongly measurable, yields a strongly measurable function given by mapping x to the product over the multiset.
Русский
Мультисет функций, каждая из которых сильно измерима, задаёт по точке x произведение значений(multiset) и является сильно измеримым.
LaTeX
$$$\forall s:\text{Multiset}(\alpha \to M), \ (\forall f \in s, \text{StronglyMeasurable } f) \Rightarrow \text{StronglyMeasurable } (a \mapsto s.prod (\lambda f, f(a)))$$$
Lean4
/-- The range of a strongly measurable function is separable. -/
protected theorem isSeparable_range {m : MeasurableSpace α} [TopologicalSpace β] (hf : StronglyMeasurable f) :
TopologicalSpace.IsSeparable (range f) :=
by
have : IsSeparable (closure (⋃ n, range (hf.approx n))) :=
.closure <| .iUnion fun n => (hf.approx n).finite_range.isSeparable
apply this.mono
rintro _ ⟨x, rfl⟩
apply mem_closure_of_tendsto (hf.tendsto_approx x)
filter_upwards with n
apply mem_iUnion_of_mem n
exact mem_range_self _
