of_subsingleton — Mathlib

English

If the index set ι is a singleton, then iIndepFun f μ holds for any family f.

Русский

Если индексный набор ι является одиночным, тогда iIndepFun f μ выполняется для любой семейства функций f.

LaTeX

$$$|\iota|=1 \Rightarrow iIndepFun(f, μ)$$$

Lean4

@[nontriviality, simp]
theorem of_subsingleton [Subsingleton ι] {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
    [IsProbabilityMeasure μ] : iIndepFun f μ :=
  Kernel.iIndepFun.of_subsingleton

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