cdf_le_one — Mathlib

English

Let μ be a measure on the real line. The cumulative distribution function Fμ is never greater than 1: for every real x, Fμ(x) ≤ 1.

Русский

Пусть μ — мера на ℝ. Функция распределения Fμ не превосходит 1: для всякого x ∈ ℝ выполняется Fμ(x) ≤ 1.

LaTeX

$$$ \forall x \in \mathbb{R}, \ cdf(\mu)(x) \le 1 $$$

Lean4

/-- The cdf is lower or equal to 1. -/
theorem cdf_le_one (x : ℝ) : cdf μ x ≤ 1 :=
  condCDF_le_one _ _ _

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