uniformOn_compl — Mathlib

English

For finite s, nonempty, we have uniformOn s t + uniformOn s t^c = 1.

Русский

Для конечного непустого s выполнено uniformOn s t + uniformOn s t^c = 1.

LaTeX

$$$uniformOn\\; s\\; t + uniformOn\\; s\\; t^c = 1$$$

Lean4

theorem uniformOn_compl (t : Set Ω) (hs : s.Finite) (hs' : s.Nonempty) : uniformOn s t + uniformOn s tᶜ = 1 := by
  rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
    (uniformOn_isProbabilityMeasure hs hs').measure_univ]

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