ceil_sub_self_eq

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.ceil_sub_self_eq

← MathLib Explorer

English

If fract(a) ≠ 0, then ⌈a⌉ − a = 1 − fract(a).

Русский

Если fract(a) ≠ 0, то ⌈a⌉ − a = 1 − fract(a).

LaTeX

$$$\\operatorname{fract}(a) \\neq 0 \\Rightarrow \\lceil a \\rceil - a = 1 - \\operatorname{fract}(a)$$$

Lean4

theorem ceil_sub_self_eq (ha : fract a ≠ 0) : (⌈a⌉ : R) - a = 1 - fract a :=
  by
  rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
  abel

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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