ceil_one

Mathlib.Algebra.Order.Floor.Semiring

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

English

For n ∈ ℕ with n ≥ 2, ⌈ofNat(n)⌉₊ = ofNat(n).

Русский

Для n ∈ ℕ, n ≥ 2: ⌈ofNat(n)⌉₊ = ofNat(n).

LaTeX

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

Lean4

@[simp]
theorem ceil_one : ⌈(1 : R)⌉₊ = 1 := by rw [← Nat.cast_one, ceil_natCast]

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

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

Разделы

Аффилиация

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