OAI/Geometry/Cannon/PlaneTopology/Hat.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonGrid.hat line 22
  2. lemma OAI.CannonGrid.hat_nonneg line 24
  3. lemma OAI.CannonGrid.continuous_hat line 26
  4. lemma OAI.CannonGrid.hat_ne_zero line 30
  5. lemma OAI.CannonGrid.hat_zero_of_one_le_abs_left line 36
  6. lemma OAI.CannonGrid.hat_zero_of_one_le_abs_right line 40
  7. lemma OAI.CannonGrid.hat_neg line 44
  8. lemma OAI.CannonGrid.hat_on_square line 49
  9. lemma OAI.CannonGrid.hat_on_square_right line 64
  10. lemma OAI.CannonGrid.hat_comm line 75
  11. lemma OAI.CannonGrid.hat_on_square_top line 79
  12. lemma OAI.CannonGrid.hat_on_square_diag line 84
  13. lemma OAI.CannonGrid.four_hats line 96
  14. lemma OAI.CannonGrid.grid_cell line 109
  15. lemma OAI.CannonGrid.nat_eq_or_succ_of_abs_lt line 118
  16. lemma OAI.CannonGrid.sum_two line 130
  17. theorem OAI.CannonGrid.grid_partition line 140
  18. abbrev OAI.CannonGrid.Square line 180
  19. abbrev OAI.CannonGrid.Index line 182
  20. def OAI.CannonGrid.vertex line 184
  21. def OAI.CannonGrid.weight line 190
  22. def OAI.CannonGrid.interpolate line 193
  23. lemma OAI.CannonGrid.weight_nonneg line 196
  24. lemma OAI.CannonGrid.weight_partition line 199
  25. lemma OAI.CannonGrid.continuous_weight line 208
  26. theorem OAI.CannonGrid.continuous_interpolate line 214
  27. lemma OAI.CannonGrid.interpolate_bounds_of_support line 220
  28. lemma OAI.CannonGrid.interpolate_bounds line 244
  29. lemma OAI.CannonGrid.interpolate_eq_of_support line 249
  30. lemma OAI.CannonGrid.support_below line 255
  31. lemma OAI.CannonGrid.support_above line 262
  32. theorem OAI.CannonGrid.interpolate_const_below line 269
  33. theorem OAI.CannonGrid.interpolate_const_above line 276
  34. theorem OAI.CannonGrid.interpolate_preserves_bands line 283
  35. theorem OAI.CannonGrid.support_dist line 314
  36. lemma OAI.CannonGrid.one_le_abs_nat_sub line 333
  37. lemma OAI.CannonGrid.weight_vertex line 342
  38. theorem OAI.CannonGrid.interpolate_vertex line 362
  39. theorem OAI.CannonGrid.interpolate_variation line 367
  40. theorem OAI.CannonGrid.exists_metric_mesh line 384