indep_iSup_of_antitone — Mathlib

English

A dual form for antitone families: independence of the supremum with m1 under IsZeroOrProbabilityMeasure μ.

Русский

Две формы для антитонных семей: независимость над Sup вместе с m1 при IsZeroOrProbabilityMeasure μ.

LaTeX

$$[IsZeroOrProbabilityMeasure μ] Indep(iSup m μ, m1 μ) под Antitone(m)$$

Lean4

theorem indep_iSup_of_antitone [SemilatticeInf ι] [IsZeroOrProbabilityMeasure μ] (h_indep : ∀ i, Indep (m i) m1 μ)
    (h_le : ∀ i, m i ≤ _mΩ) (h_le' : m1 ≤ _mΩ) (hm : Antitone m) : Indep (⨆ i, m i) m1 μ :=
  Kernel.indep_iSup_of_antitone h_indep h_le h_le' hm

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