truncateToReal_le

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.truncateToReal_le

← MathLib Explorer

English

For t ≠ ∞, and any x, truncateToReal t x ≤ t.toReal.

Русский

Для t ≠ ∞ верно truncateToReal t x ≤ t.toReal для любого x.

LaTeX

$$$\truncateToReal(t, x) \leq t.toReal$$$

Lean4

theorem truncateToReal_le {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) {x : ℝ≥0∞} : truncateToReal t x ≤ t.toReal :=
  by
  rw [truncateToReal]
  gcongr
  exacts [t_ne_top, min_le_left t x]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru