of_subsingleton — Mathlib

English

If the index set is a singleton, then iCondIndepFun m' hm' f μ holds trivially.

Русский

Если множество индексов единичное, условная независимость iCondIndepFun выполняется тривиально.

LaTeX

$$$\\text{If } ι \\text{ is a singleton, then } iCondIndepFun(m',hm',f,μ)$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton ι] : iCondIndepFun m' hm' f μ :=
  Kernel.iIndepFun.of_subsingleton

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