OAI/Geometry/PlaneColoring/Covering.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem160.triangular_wedge_bound line 9
2. theorem OAI.Problem160.triangular_rectangle_cover line 21
3. theorem OAI.Problem160.triangular_lattice_cover line 47

   Source documentation

   Every point in the plane is within squared distance 1/3 of the unit triangular lattice. The proof gives one of three explicit nearby centers.

   theorem triangular_lattice_cover (x y : ℝ) :
       ∃ m n : ℤ,
         (x - ((m : ℝ) + (n : ℝ) / 2)) ^ 2 +
           (y - Real.sqrt 3 * (n : ℝ) / 2) ^ 2 ≤ 1 / 3 := by
   …