indep

Mathlib.Probability.Independence.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.iIndep.indep

English

If iIndep m μ holds, then for any i ≠ j we have Indep(m_i, m_j; μ).

Русский

Если выполняется iIndep m μ, то для любых i ≠ j выполняется Indep(m_i, m_j; μ).

LaTeX

$$iIndep m μ ⇒ ∀ i j, i ≠ j ⇒ Indep(m_i, m_j; μ)$$

Lean4

theorem indep (h_indep : iIndep m μ) {i j : ι} (hij : i ≠ j) : Indep (m i) (m j) μ :=
  Kernel.iIndep.indep h_indep hij

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru