aestronglyMeasurable_union_iff — Mathlib

English

AEStronglyMeasurable on μ.restrict(s ∪ t) is equivalent to AEStronglyMeasurable on μ.restrict s and μ.restrict t.

Русский

AEStronglyMeasurable на ограничении по s∪t равно AEStronglyMeasurable на ограничениях по s и по t.

LaTeX

$$$\text{AEStronglyMeasurable}(f, μ.restrict(s \cup t)) \iff \text{AEStronglyMeasurable}(f, μ.restrict(s)) \land \text{AEStronglyMeasurable}(f, μ.restrict(t)).$$$

Lean4

@[simp]
theorem _root_.aestronglyMeasurable_union_iff [PseudoMetrizableSpace β] {s t : Set α} :
    AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔
      AEStronglyMeasurable f (μ.restrict s) ∧ AEStronglyMeasurable f (μ.restrict t) :=
  by simp only [union_eq_iUnion, aestronglyMeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

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