natFloor_natCast_div_natCast

Mathlib.Data.Rat.Floor

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

← MathLib Explorer

English

ℚ is denumerable; there exists a bijection with ℕ.

Русский

ℚ денумирабельно — существует биекция с ℕ.

LaTeX

$$$\exists f:\mathbb{N}\to\mathbb{Q}\text{ bijective}$$$

Lean4

@[norm_cast]
theorem natFloor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d :=
  by
  rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]
  push_cast
  exact floor_intCast_div_natCast n d

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

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

Разделы

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

Аффилиация

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