indep_limsup_atBot_self — Mathlib

English

In the kernel setting, the tail limsup atBot is independent of itself: Indep(limsup s atBot) (limsup s atBot) κ μα.

Русский

В рамках ядра хвостовая limsup atBot независима сама от себя.

LaTeX

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

Lean4

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

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