truncateToReal_eq_toReal — Mathlib

English

If t is not the top element and x ≤ t, then truncateToReal(t, x) equals x.toReal.

Русский

Если t не максимальное и x ≤ t, то truncateToReal(t, x) равно x.toReal.

LaTeX

$$$\text{truncateToReal}(t, x) = x^{\mathrm{toReal}}$$$

Lean4

theorem truncateToReal_eq_toReal {t x : ℝ≥0∞} (t_ne_top : t ≠ ∞) (x_le : x ≤ t) : truncateToReal t x = x.toReal :=
  by
  have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top
  have obs : min t x ≠ ∞ := by simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]
  exact (ENNReal.toReal_eq_toReal obs x_lt_top.ne).mpr (min_eq_right x_le)

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