English
The map toWeakDualBCNN is an embedding: it is injective and induces the topology.
Русский
Отображение toWeakDualBCNN является вложением: инъективно и индуцирует топологию.
LaTeX
$$$ \text{IsEmbedding} (toWeakDualBCNN : \text{FiniteMeasure } \Omega \to WeakDual \mathbb{R}_{\ge 0} (\Omega \to^{} \mathbb{R}_{\ge 0})). $$$
Lean4
/-- The mapping `toWeakDualBCNN` from finite Borel measures to the weak dual of `Ω →ᵇ ℝ≥0` is
injective, if in the underlying space `Ω`, indicator functions of closed sets have decreasing
approximations by sequences of continuous functions (in particular if `Ω` is pseudometrizable). -/
theorem injective_toWeakDualBCNN : Injective (toWeakDualBCNN : FiniteMeasure Ω → WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) :=
by
intro μ ν hμν
apply ext_of_forall_lintegral_eq
intro f
have key := congr_fun (congrArg DFunLike.coe hμν) f
apply (ENNReal.toNNReal_eq_toNNReal_iff' ?_ ?_).mp key
· exact (lintegral_lt_top_of_nnreal μ f).ne
· exact (lintegral_lt_top_of_nnreal ν f).ne
