toNNReal_le_one_iff

Mathlib.Data.Int.WithZero

URI: https://scilib.ai/kg/mathlib#WithZeroMulInt.toNNReal_le_one_iff

← MathLib Explorer

English

For e with 1 < e, toNNReal(ne_zero_of_lt he) m ≤ 1 iff m ≤ 1.

Русский

Для e с 1 < e, toNNReal(ne_zero_of_lt he) m ≤ 1 тогда и только если m ≤ 1.

LaTeX

$$toNNReal(ne_zero_of_lt) m \le 1 \Leftrightarrow m \le 1$$

Lean4

theorem toNNReal_le_one_iff {e : ℝ≥0} {m : ℤᵐ⁰} (he : 1 < e) : toNNReal (ne_zero_of_lt he) m ≤ 1 ↔ m ≤ 1 := by
  rw [← (toNNReal_strictMono he).le_iff_le, map_one]

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

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

Разделы

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

Аффилиация

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