indep_bot_right — Mathlib

English

If ι is a subsingleton, iIndepSets m κ μ holds trivially for Markov kernels.

Русский

Если ι является субодинотонным, iIndepSets m κ μ тривиально выполняется для марковских ядер.

LaTeX

$$$ [Subsingleton\\ ι] \\; iIndepSets m κ μ $$$

Lean4

theorem indep_bot_right (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    [IsZeroOrMarkovKernel κ] : Indep m' ⊥ κ μ := by
  intro s t _ ht
  rw [Set.mem_setOf_eq, MeasurableSpace.measurableSet_bot_iff] at ht
  rcases eq_zero_or_isMarkovKernel κ with rfl | h
  · simp
  refine Filter.Eventually.of_forall (fun a ↦ ?_)
  rcases ht with ht | ht
  · rw [ht, Set.inter_empty, measure_empty, mul_zero]
  · rw [ht, Set.inter_univ, measure_univ, mul_one]

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