fract_eq_zero_or_add_one_sub_ceil

English

For any a, either fract(a) = 0 or fract(a) = a + 1 − ⌈a⌉.

Русский

Для любого a либо дробная часть fract(a) равна 0, либо fract(a) = a + 1 − ⌈a⌉.

LaTeX

$$$\\operatorname{fract}(a) = 0 \\;\\lor\\; \\operatorname{fract}(a) = a + 1 - \\lceil a \\rceil$$$

Lean4

theorem fract_eq_zero_or_add_one_sub_ceil (a : R) : fract a = 0 ∨ fract a = a + 1 - (⌈a⌉ : R) :=
  by
  rcases eq_or_ne (fract a) 0 with ha | ha
  · exact Or.inl ha
  right
  suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel
  norm_cast
  rw [ceil_eq_iff]
  refine ⟨?_, _root_.le_of_lt <| by simp⟩
  rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
  exact ha.symm.lt_of_le (fract_nonneg a)

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