condExpInd_disjoint_union_apply — Mathlib

English

Under measurability and finiteness assumptions, condExpInd on s ∪ t equals the sum of condExpInd on s and on t for any x.

Русский

При измеримости и конечности condExpInd на s ∪ t равен сумме condExpInd на s и condExpInd на t.

LaTeX

$$$ condExpInd\; G\; hm\; \mu\; (s \cup t)\; x = condExpInd\; G\; hm\; \mu\; s\; x + condExpInd\; G\; hm\; \mu\; t\; x,$$

Lean4

theorem condExpInd_disjoint_union_apply (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞)
    (hst : Disjoint s t) (x : G) : condExpInd G hm μ (s ∪ t) x = condExpInd G hm μ s x + condExpInd G hm μ t x :=
  condExpIndL1_disjoint_union hs ht hμs hμt hst x

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