English
Countable union across indices of measurably separable pairs remains measurably separable.
Русский
Счетное объединение по индексам пар образов сохраняет свойство измеримого разделения.
LaTeX
$$$[Countable ι] \; {s t : ι \to Set α}, \; (∀ m n, MeasurablySeparable (s m) (t n)) \Rightarrow MeasurablySeparable (\bigcup_n s n) (\bigcup_m t m).$$$
Lean4
theorem iUnion [Countable ι] {α : Type*} [MeasurableSpace α] {s t : ι → Set α}
(h : ∀ m n, MeasurablySeparable (s m) (t n)) : MeasurablySeparable (⋃ n, s n) (⋃ m, t m) :=
by
choose u hsu htu hu using h
refine ⟨⋃ m, ⋂ n, u m n, ?_, ?_, ?_⟩
· refine iUnion_subset fun m => subset_iUnion_of_subset m ?_
exact subset_iInter fun n => hsu m n
· simp_rw [disjoint_iUnion_left, disjoint_iUnion_right]
intro n m
apply Disjoint.mono_right _ (htu m n)
apply iInter_subset
· refine MeasurableSet.iUnion fun m => ?_
exact MeasurableSet.iInter fun n => hu m n
