prob_le_one — Mathlib

English

For IsZeroOrProbabilityMeasure μ, the real-valued measure μ.real on any set s satisfies μ.real s ≤ 1.

Русский

Для μ с нулевой или вероятностной мерой, вещественное значение меры на любой множество удовлетворяет μ.real(s) ≤ 1.

LaTeX

$$\mu.real s ≤ 1$$

Lean4

theorem prob_le_one {μ : Measure α} [IsZeroOrProbabilityMeasure μ] {s : Set α} : μ s ≤ 1 :=
  by
  apply (measure_mono (subset_univ _)).trans
  rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h <;> simp [h]

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