instIsZeroOrProbabilityMeasureUniformOn

English

The construction uniformOn s yields either the zero measure or a probability measure; in particular, if s is finite and nonempty it is a probability measure.

Русский

Конструкция uniformOn s даёт либо нулевую меру, либо меру вероятностей; в частности, если s конечна и непустая, то это вероятность.

LaTeX

$$$\text{uniformOn}(s) \text{ is a probability measure when } s\text{ is finite and nonempty.}$$$

Lean4

instance {s : Set Ω} : IsZeroOrProbabilityMeasure (uniformOn s) := by unfold uniformOn; infer_instance

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