English
Let f: ι → α → β and g: α → β be pointwise defined. If each f(n) is strongly measurable and g is strongly measurable, then for every fixed n and j the set of points x where the sequence (f(k, x)) does not converge to g(x) (as k → ∞ in the index set) is a measurable subset of α.
Русский
Пусть f: ι → α → β и g: α → β заданы. Если каждый f(n) является сильно измеримой, а g является сильно измеримой, то для всякого фиксированного n и j множество точек x ∈ α, для которых последовательность (f(k, x)) не сходится к g(x) при k → ∞ по индексу ι, является измеримым.
LaTeX
$$$\forall n, j,\; \text{MeasurableSet}(\text{notConvergentSeq } f g n j)$.$$
Lean4
theorem notConvergentSeq_measurableSet [Preorder ι] [Countable ι] (hf : ∀ n, StronglyMeasurable[m] (f n))
(hg : StronglyMeasurable g) : MeasurableSet (notConvergentSeq f g n j) :=
MeasurableSet.iUnion fun k =>
MeasurableSet.iUnion fun _ => StronglyMeasurable.measurableSet_lt stronglyMeasurable_const <| (hf k).edist hg
