stronglyMeasurable_of_mulSupport_subset_isCompact

English

A continuous function whose support is contained in a compact set is strongly measurable.

Русский

Непрерывная функция с опорой, contained in компакт, сильно измерима.

LaTeX

$$$\text{Continuous}(f) \land \text{IsCompact}(k) \land \mathrm{mulSupport}(f) \subseteq k \Rightarrow \mathrm{StronglyMeasurable}(f)$$$

Lean4

/-- A continuous function whose support is contained in a compact set is strongly measurable. -/
@[to_additive]
theorem _root_.Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact [MeasurableSpace α] [TopologicalSpace α]
    [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [One β]
    {f : α → β} (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : mulSupport f ⊆ k) : StronglyMeasurable f :=
  by
  letI : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
  rw [stronglyMeasurable_iff_measurable_separable]
  exact ⟨hf.measurable, (isCompact_range_of_mulSupport_subset_isCompact hf hk h'f).isSeparable⟩

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