English
OpensMeasurableSpace for the product of a countable family of spaces, i.e., OpensMeasurableSpace ((i:ι) → X i).
Русский
Продукты по индексу счётной множества обладают OpensMeasurableSpace.
LaTeX
$$$\\text{OpensMeasurableSpace}(\\forall i, X_i)$$$
Lean4
instance opensMeasurableSpace {ι : Type*} {X : ι → Type*} [Countable ι] [t' : ∀ i, TopologicalSpace (X i)]
[∀ i, MeasurableSpace (X i)] [∀ i, SecondCountableTopology (X i)] [∀ i, OpensMeasurableSpace (X i)] :
OpensMeasurableSpace (∀ i, X i) := by
constructor
have :
Pi.topologicalSpace =
.generateFrom
{t | ∃ (s : ∀ a, Set (X a)) (i : Finset ι), (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = pi (↑i) s} :=
by simp only [funext fun a => @eq_generateFrom_countableBasis (X a) _ _, pi_generateFrom_eq]
rw [borel_eq_generateFrom_of_subbasis this]
apply generateFrom_le
rintro _ ⟨s, i, hi, rfl⟩
refine MeasurableSet.pi i.countable_toSet fun a ha => IsOpen.measurableSet ?_
rw [eq_generateFrom_countableBasis (X a)]
exact .basic _ (hi a ha)
