ceil_ofNat

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.ceil_ofNat

English

Ceiling of a natural-cast equals the natural itself for n ≥ 2.

Русский

Округление вверх от натурального числа равно самому числу при n ≥ 2.

LaTeX

$$$$\forall n \in \mathbb{N},\ [n \ge 2] \Rightarrow \left\lceil \mathrm{ofNat}(n) \right\rceil = \mathrm{ofNat}(n).$$$$

Lean4

@[simp]
theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈(ofNat(n) : R)⌉₊ = ofNat(n) :=
  ceil_natCast n

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

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

Разделы

Аффилиация

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