convergent_zero

Mathlib.NumberTheory.DiophantineApproximation.Basic

URI: https://scilib.ai/kg/mathlib#Real.convergent_zero

English

The zeroth convergent of ξ is ⌊ξ⌋.

Русский

Нулевой конвергент числа ξ равен ⌊ξ⌋.

LaTeX

$$$$\\xi.convergent 0 = \\lfloor \\xi \\rfloor.$$$$

Lean4

/-- The zeroth convergent of `ξ` is `⌊ξ⌋`. -/
@[simp]
theorem convergent_zero (ξ : ℝ) : ξ.convergent 0 = ⌊ξ⌋ :=
  rfl

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

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

Разделы

Аффилиация

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