floor_cast

Mathlib.Data.Rat.Floor

URI: https://scilib.ai/kg/mathlib#Rat.floor_cast

English

ℚ admits an encoding into natural numbers; i.e., it is encodable.

Русский

ℚ имеет кодирование в ℕ; т.е. кодируемо.

LaTeX

$$Encodable \mathbb{Q}$$

Lean4

@[simp, norm_cast]
theorem floor_cast (x : ℚ) : ⌊(x : α)⌋ = ⌊x⌋ :=
  floor_eq_iff.2 (mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋))

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

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

Разделы

Аффилиация

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