Lean4
/-- If either `α` or `β` has second-countable topology, then the open sets in `α × β` belong to the
product sigma-algebra. -/
instance opensMeasurableSpace [h : SecondCountableTopologyEither α β] : OpensMeasurableSpace (α × β) :=
by
apply opensMeasurableSpace_iff_forall_measurableSet.2 (fun s hs ↦ ?_)
rcases h.out with hα | hβ
· let F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
have A : ∀ a, IsOpen (F a) := by
intro a
apply isOpen_iff_forall_mem_open.2
rintro y ⟨b, b_open, yb, hb⟩
exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
have : s = ⋃ a ∈ countableBasis α, a ×ˢ F a := by
apply Subset.antisymm
· rintro ⟨y1, y2⟩ hy
rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis α, y1 ∈ a ∧ a ⊆ u :=
IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis α) yu u_open
simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
exact ⟨a, ya, ha, v, v_open, yv, (Set.prod_mono_left au).trans huv⟩
· rintro ⟨y1, y2⟩ hy
simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
exact hb (mem_prod.2 ⟨ya, yb⟩)
rw [this]
apply MeasurableSet.biUnion (countable_countableBasis α) (fun a ha ↦ ?_)
exact (isOpen_of_mem_countableBasis ha).measurableSet.prod (A a).measurableSet
· let F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
have A : ∀ a, IsOpen (F a) := by
intro a
apply isOpen_iff_forall_mem_open.2
rintro y ⟨b, b_open, yb, hb⟩
exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
have : s = ⋃ a ∈ countableBasis β, F a ×ˢ a := by
apply Subset.antisymm
· rintro ⟨y1, y2⟩ hy
rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop]
exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩
· rintro ⟨y1, y2⟩ hy
simp only [mem_iUnion, mem_prod, exists_and_left, exists_prop] at hy
rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
exact hb (mem_prod.2 ⟨yb, ya⟩)
rw [this]
apply MeasurableSet.biUnion (countable_countableBasis β) (fun a ha ↦ ?_)
exact (A a).measurableSet.prod (isOpen_of_mem_countableBasis ha).measurableSet
