trajContent_ne_top — Mathlib

English

Let A(n) be a decreasing sequence of cylinders with empty intersection and each A(n) ∈ measurable cylinders. Then trajContent κ x0 (A(n)) tends to 0 as n → ∞.

Русский

Пусть A(n) — убывающая последовательность цилиндров с пустым пересечением и каждый A(n) ∈ измеримых цилиндров. Тогда trajContent κ x0 (A(n)) стягивается к 0 при n → ∞.

LaTeX

$$$\\forall A:\\mathbb{N}\\to Set(\\prod n, X_n),\\ A\\_mem:\\ A(n) \\in measurableCylinders X,\\ A\\_anti:\\ Antitone A,\\ A\\inter:\\bigcap_n A(n)=\\emptyset\\Rightarrow\\ Tendsto\\bigl(n\\mapsto trajContent\\ κ\\ x_0\\ (A(n))\\bigr)\\ atTop\\ (\\mathcal{N} 0)$$$

Lean4

theorem trajContent_ne_top {a : ℕ} {x : Π i : Iic a, X i} {s : Set (Π n, X n)} : trajContent κ x s ≠ ∞ :=
  projectiveFamilyContent_ne_top (isProjectiveMeasureFamily_partialTraj κ x)

Похожие утверждения