monotone_truncateToReal — Mathlib

English

For any t ≠ ∞, the map x ↦ truncateToReal t x is monotone increasing in x.

Русский

Для любого t ≠ ∞ отображение x ↦ truncateToReal t x инкрементально по x.

LaTeX

$$$\text{Monotone}(\lambda x. \text{truncateToReal}(t, x))$$$

Lean4

/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is monotone when `t ≠ ∞`. -/
theorem monotone_truncateToReal {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) : Monotone (truncateToReal t) :=
  by
  intro x y x_le_y
  simp only [truncateToReal]
  gcongr
  exact ne_top_of_le_ne_top t_ne_top (min_le_left _ _)

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