ceil_coe

Mathlib.Data.NNRat.Floor

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

English

For any q ∈ ℚ≥0, the ceiling of q, when coerced to ℕ, equals the ceiling of q viewed in ℚ.

Русский

Для любого q ∈ ℚ≥0, верхняя целая часть q после приведения к ℕ равна ceil(q) в ℚ.

LaTeX

$$∀ q ∈ ℚ_{≥0}, ⌈q⌉_{+} = ⌈q⌉$$

Lean4

@[simp, norm_cast]
theorem ceil_coe (q : ℚ≥0) : ⌈(q : ℚ)⌉₊ = ⌈q⌉₊ :=
  rfl

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

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

Разделы

Аффилиация

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