English
A continuous function on a product X×Y with compact support is measurable with respect to the product Borel sigma-algebra.
Русский
Пусть непрерывная функция на произведении X×Y имеет компактную опору; тогда она измерима относительно произведённой борелевой сигм-алгебры.
LaTeX
$$$f: X\\times Y \\to \\alpha$ непрерывна и имеет компактную опору \\Rightarrow f\\text{ измерима w.r.t. } \\mathcal{B}(X\\times Y).$$$
Lean4
/-- A continuous function with compact support on a product space is measurable for the product
sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions. -/
theorem measurable_of_prod [TopologicalSpace α] [PseudoMetrizableSpace α] [MeasurableSpace α] [BorelSpace α]
{f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) : Measurable f :=
by
letI : PseudoMetricSpace α := TopologicalSpace.pseudoMetrizableSpacePseudoMetric α
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto (0 : ℝ)
have : ∀ n, ∃ (g : SimpleFunc (X × Y) α), ∀ x, dist (f x) (g x) < u n := fun n ↦
h'f.exists_simpleFunc_approx_of_prod hf (u_pos n)
choose g hg using this
have A : ∀ x, Tendsto (fun n ↦ g n x) atTop (𝓝 (f x)) :=
by
intro x
rw [tendsto_iff_dist_tendsto_zero]
apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim
rw [dist_comm]
exact (hg n x).le
apply measurable_of_tendsto_metrizable (fun n ↦ (g n).measurable) (tendsto_pi_nhds.2 A)
