uniformOn_isProbabilityMeasure — Mathlib

English

For finite s, uniformOn s t = 0 iff s ∩ t = ∅.

Русский

Для конечного s, uniformOn s t = 0 тогда и только тогда, когда s ∩ t = ∅.

LaTeX

$$$uniformOn(s)(t) = 0 \iff s \cap t = \varnothing$$$

Lean4

theorem uniformOn_isProbabilityMeasure {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
    IsProbabilityMeasure (uniformOn s) :=
  by
  apply cond_isProbabilityMeasure_of_finite
  · rwa [Measure.count_ne_zero_iff]
  · exact (Measure.count_apply_lt_top.2 hs).ne

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