continuous_truncateToReal — Mathlib

English

The truncated real-valued map is continuous in its argument when the truncation level t is finite.

Русский

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

LaTeX

$$$\text{Continuous}(\text{truncateToReal}(t))$ при $t \neq \infty$$$

Lean4

/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is continuous when `t ≠ ∞`. -/
@[fun_prop]
theorem continuous_truncateToReal {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) : Continuous (truncateToReal t) :=
  by
  apply continuousOn_toReal.comp_continuous (by fun_prop)
  simp [t_ne_top]

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