fract_neg — Mathlib

English

If fract(x) ≠ 0, then fract(-x) = 1 − fract(x).

Русский

Если fract(x) ≠ 0, то fract(-x) = 1 − fract(x).

LaTeX

$$$\\\\operatorname{fract}(-x) = 1 - \\\\operatorname{fract}(x), \\text{ если } \\\\operatorname{fract}(x) \\\\neq 0$$$

Lean4

theorem fract_neg {x : R} (hx : fract x ≠ 0) : fract (-x) = 1 - fract x :=
  by
  rw [fract_eq_iff]
  constructor
  · rw [le_sub_iff_add_le, zero_add]
    exact (fract_lt_one x).le
  refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 1, ?_⟩
  simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]
  conv in -x => rw [← floor_add_fract x]
  simp [-floor_add_fract]

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