OAI/Geometry/PlaneColoring/Metric.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem160.triangularLattice line 10

   Source documentation

   Triangular lattice with nearest-neighbor spacing 4/5.

   def triangularLattice (a b : ℤ) : Plane :=
   …

   Mentions: OAI.Problem160.Plane

2. theorem OAI.Problem160.triangularLattice_zero line 14
3. theorem OAI.Problem160.triangularLattice_one line 17
4. theorem OAI.Problem160.triangularLattice_norm_sq line 20
5. theorem OAI.Problem160.triangularLattice_sub line 29
6. theorem OAI.Problem160.triangularLattice_dist_sq line 34
7. theorem OAI.Problem160.triangularLattice_dist_gt_two line 40
8. theorem OAI.Problem160.dist_triangularLattice_sq line 50
9. theorem OAI.Problem160.dist_triangularLattice_le_of_coordinates line 60