measure_eq_zero_or_one_of_indepSet_self

English

Let h_indep be an independence of t with itself under κ μα; then κ a t ∈ {0,1} almost everywhere.

Русский

Пусть т независим с самим собой по κ μα; тогда κ a t ∈ {0,1} почти наверняка.

LaTeX

$$$\\forall a, \\kappa a t \\in \\{0,1\\}$$$

Lean4

theorem measure_eq_zero_or_one_of_indepSet_self [h : ∀ a, IsFiniteMeasure (κ a)] {t : Set Ω}
    (h_indep : IndepSet t t κ μα) : ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1 :=
  Kernel.measure_eq_zero_or_one_of_indepSet_self' (ae_of_all μα h) h_indep

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