pith. machine review for the scientific record. sign in
theorem proved tactic proof

distZ_le_half

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  44theorem distZ_le_half (δ : ℝ) : distZ δ ≤ 1 / 2 := by

proof body

Tactic-mode proof.

  45  unfold distZ
  46  rcases le_or_gt (Int.fract δ) (1 / 2) with h | h
  47  · exact min_le_left _ _ |>.trans h
  48  · have : 1 - Int.fract δ ≤ 1 / 2 := by linarith
  49    exact min_le_right _ _ |>.trans this
  50
  51/-- d_ℤ is 1-periodic: d_ℤ(δ + n) = d_ℤ(δ) for integer n. -/

depends on (6)

Lean names referenced from this declaration's body.