measure_eq_zero_or_one_of_indepSet_self'

English

If μα-almost surely κ a t is finite, then κ a t ∈ {0,1}.

Русский

Если почти наверняка κ a t конечна, то κ 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 :=
  by
  filter_upwards [measure_eq_zero_or_one_or_top_of_indepSet_self h_indep, h] with a h_0_1_top h'
  simpa only [measure_ne_top (κ a), or_false] using h_0_1_top

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