fract_eq_self

Mathlib.Algebra.Order.Floor.Ring

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

English

The fractional part of a equals a exactly when a lies in the interval [0,1).

Русский

Дробная часть числа fract(a) равна а тогда и только тогда, когда a ∈ [0,1).

LaTeX

$$$\\\\operatorname{fract}(a) = a \\\\iff 0 \\\\le a \\\\land a < 1$$$

Lean4

@[simp]
theorem fract_eq_self {a : R} : fract a = a ↔ 0 ≤ a ∧ a < 1 :=
  fract_eq_iff.trans <| and_assoc.symm.trans <| and_iff_left ⟨0, by simp⟩

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

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

Разделы

Аффилиация

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