uniformOn_union — Mathlib

English

For finite s, t, u with t and u disjoint, the union formula holds: uniformOn s (t ∪ u) = uniformOn s t + uniformOn s u.

Русский

Для конечных s,t,u при условии дисjoint, выполняется uniformOn s (t ∪ u) = uniformOn s t + uniformOn s u.

LaTeX

$$$uniformOn\\; s\\ (t \\cup u) = uniformOn\\; s\\; t + uniformOn\\; s\\; u$$$

Lean4

theorem uniformOn_union (hs : s.Finite) (htu : Disjoint t u) : uniformOn s (t ∪ u) = uniformOn s t + uniformOn s u :=
  by
  rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    Set.inter_union_distrib_left, measure_union, mul_add]
  exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]

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