ceil_sub_one

Mathlib.Algebra.Order.Floor.Semiring

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

English

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

Русский

Пусть a ∈ R, n ∈ ℕ, n ≥ 2. Тогда ⌈a − ofNat(n)⌉₊ = ⌈a⌉₊ − ofNat(n).

LaTeX

$$$$ \\lceil a - \\operatorname{ofNat}(n) \\rceil_+ = \\lceil a \\rceil_+ - \\operatorname{ofNat}(n) $$$$

Lean4

@[simp]
theorem ceil_sub_one (a : R) : ⌈a - 1⌉₊ = ⌈a⌉₊ - 1 := by simpa using ceil_sub_natCast a 1

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

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

Разделы

Аффилиация

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