exists_nat_pos_inv_lt

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.exists_nat_pos_inv_lt

English

For b > 0 in ℝ≥0, there exists n ∈ ℕ with 0 < n and n^{-1} < b.

Русский

Для b > 0 в ℝ≥0 существует n ∈ ℕ такое, что 0 < n и n^{-1} < b.

LaTeX

$$$\forall b > 0\ in\ \mathbb{R}_{\ge 0},\ exists\ n \in \mathbb{N},\ 0 < n \land n^{-1} < b$$$

Lean4

theorem exists_nat_pos_inv_lt {b : ℝ≥0} (hb : 0 < b) : ∃ (n : ℕ), 0 < n ∧ (n : ℝ≥0)⁻¹ < b :=
  b.toReal.exists_nat_pos_inv_lt hb

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

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

Разделы

Аффилиация

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