coe_floor

Mathlib.Data.NNRat.Floor

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

English

The natural floor of q, when cast to integers, equals the floor of q cast to integers; i.e., ↑⌊q⌋₊ = ⌊q⌋.

Русский

Целая часть q через приведение к целым равна ⌊q⌋, т.е. ↑⌊q⌋₊ = ⌊q⌋.

LaTeX

$$∀ q ∈ ℚ≥0, ↑⌊q⌋₊ = ⌊q⌋$$

Lean4

@[simp, norm_cast]
theorem coe_floor (q : ℚ≥0) : ↑⌊q⌋₊ = ⌊(q : ℚ)⌋ :=
  Int.natCast_floor_eq_floor q.coe_nonneg

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

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

Разделы

Аффилиация

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