coe_le_iff

Mathlib.Data.ENNReal.Basic

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

English

For ENNReal a and NNReal r, a ↑≤ a iff ∀ p, a = p → r ≤ p.

Русский

Для ENNReal a и NNReal r, a ≤ ↑r эквивалентно ∀ p, a = p → r ≤ p.

LaTeX

$$$ \uparrow r \le a \iff \forall p : \mathbb{R}_{\\ge 0}, a = p \rightarrow r \le p $$$

Lean4

theorem coe_le_iff : ↑r ≤ a ↔ ∀ p : ℝ≥0, a = p → r ≤ p :=
  WithTop.coe_le_iff

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

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

Разделы

Аффилиация

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