intFloor_cast

Mathlib.Data.NNRat.Floor

URI: https://scilib.ai/kg/mathlib#NNRat.intFloor_cast

← MathLib Explorer

English

For x ∈ ℚ≥0, the integer floor of x viewed in K equals the integer floor of x viewed in ℚ≥0.

Русский

Для x ∈ ℚ≥0 целая часть x в K равна целой части x в ℚ≥0.

LaTeX

$$⌊x⌋_{K} = ⌊x⌋$$

Lean4

@[simp, norm_cast]
theorem intFloor_cast (x : ℚ≥0) : ⌊(x : K)⌋ = ⌊(x : ℚ)⌋ :=
  by
  rw [Int.floor_eq_iff, ← coe_floor]
  norm_cast
  norm_cast
  rw [Nat.cast_add_one, ← Nat.floor_eq_iff (zero_le _)]

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

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

Разделы

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

Аффилиация

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