defaultRatCDF — Mathlib

English

The function q ↦ 0 if q<0 else 1.

Русский

Функция q ↦ 0 если q<0, иначе 1.

LaTeX

$$$defaultRatCDF(q) = \\begin{cases}0 & q<0 \\\\ 1 & q\\ge 0\\end{cases}$$$

Lean4

/-- A function with the property `IsMeasurableRatCDF`.
Used in a piecewise construction to convert a function which only satisfies the properties
defining `IsMeasurableRatCDF` on some set into a true `IsMeasurableRatCDF`. -/
def defaultRatCDF (q : ℚ) :=
  if q < 0 then (0 : ℝ) else 1

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