indep_limsup_self — Mathlib

English

Under standard assumptions, the limsup of s with itself is independent with itself under κ and μ.

Русский

При стандартных предположениях limsup s с самим собой независимо относительно κ и μ.

LaTeX

$$$\\text{Indep}\\left(\\limsup s f, \\limsup s f\\right)\\kappa\\mu$$$

Lean4

theorem indep_limsup_self (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) (hf : ∀ t, p t → tᶜ ∈ f)
    (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a)) (hns_univ : ∀ n, ∃ a, n ∈ ns a) :
    Indep (limsup s f) (limsup s f) κ μα :=
  indep_of_indep_of_le_left (indep_iSup_limsup h_le h_indep hf hns hnsp hns_univ) limsup_le_iSup

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