iIndepSets — Mathlib

English

If each m_n equals generateFrom(s_n) and iIndep m μ holds, then s is iIndepSets from μ.

Русский

Если для каждого n выполняется m_n = generateFrom(s_n) и iIndep m μ, тогда s является iIndepSets относительно μ.

LaTeX

$$ (∀ n, m_n = generateFrom(s_n)) ∧ iIndep m μ ⇒ iIndepSets s μ$$

Lean4

theorem iIndepSets {s : ι → Set (Set Ω)} (hms : ∀ n, m n = generateFrom (s n)) (h_indep : iIndep m μ) :
    iIndepSets s μ :=
  Kernel.iIndep.iIndepSets hms h_indep

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