indep_limsup_atTop_self — Mathlib

English

In the kernel setting, the limsup along atTop is independent from itself with kernel κ and measure μα: Indep(limsup s atTop, limsup s atTop) κ μα.

Русский

В настройке ядра независимость limsup вдоль atTop от самого себя: Indep(limsup s atTop, limsup s atTop) κ μα.

LaTeX

$$$\Indep(\limsup s atTop, \limsup s atTop)\; κ\; μα$$$

Lean4

theorem indep_limsup_atTop_self (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s μ) :
    Indep (limsup s atTop) (limsup s atTop) μ :=
  Kernel.indep_limsup_atTop_self h_le h_indep

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