separableSpace_range_union_singleton

English

If f is strongly measurable, the range of f together with any fixed point forms a separable space.

Русский

Если f сильно измерима, то множество значений f вместе с фиксированной точкой образуют сепарабельное пространство.

LaTeX

$$$\forall f: \alpha \to β, \text{StronglyMeasurable } f \Rightarrow \text{SeparableSpace }(\operatorname{range} f \cup \{ b \})$$$

Lean4

theorem separableSpace_range_union_singleton {_ : MeasurableSpace α} [TopologicalSpace β] [PseudoMetrizableSpace β]
    (hf : StronglyMeasurable f) {b : β} : SeparableSpace (range f ∪ { b } : Set β) :=
  letI := pseudoMetrizableSpacePseudoMetric β
  (hf.isSeparable_range.union (finite_singleton _).isSeparable).separableSpace

Похожие утверждения