truncateToReal — Mathlib

English

The truncated casting map truncates an extended nonnegative real to a real by taking the minimum with a cut-off t and then converting to a real.

Русский

Обрезанное отображение переводит бесконечно неотрицательное число в действительное путём взятия минимума с порогом t и приведения к действительному.

LaTeX

$$$\text{truncateToReal}(t, x) = (\min\,t\,x).toReal$$$

Lean4

/-- With truncation level `t`, the truncated cast `ℝ≥0∞ → ℝ` is given by `x ↦ (min t x).toReal`.
Unlike `ENNReal.toReal`, this cast is continuous and monotone when `t ≠ ∞`. -/
noncomputable def truncateToReal (t x : ℝ≥0∞) : ℝ :=
  (min t x).toReal

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