measure_eq_zero_or_one_or_top_of_indepSet_self

English

If t is independent with itself under κ and μα, then the measure κ a t is 0 or 1 (almost everywhere in a).

Русский

Если множество t независимо само относительно ядра κ и меры μα, то мера κ а t равна 0 или 1 (почти всюду по a).

LaTeX

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

Lean4

theorem measure_eq_zero_or_one_or_top_of_indepSet_self {t : Set Ω} (h_indep : IndepSet t t μ) :
    μ t = 0 ∨ μ t = 1 ∨ μ t = ∞ := by
  simpa only [ae_dirac_eq, Filter.eventually_pure] using Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self h_indep

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