OAI/Analysis/NodalLength/Cells.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpNodal.Grid.Cell line 215
  2. def OAI.SharpNodal.Grid.Cell.side line 220
  3. def OAI.SharpNodal.Grid.Cell.points line 221
  4. def OAI.SharpNodal.Grid.Cell.near line 222
  5. lemma OAI.SharpNodal.Grid.Cell.card_points line 224
  6. lemma OAI.SharpNodal.Grid.Cell.card_near line 225
  7. lemma OAI.SharpNodal.Grid.Cell.side_pos line 227
  8. lemma OAI.SharpNodal.Grid.Cell.side_mono line 228
  9. lemma OAI.SharpNodal.Grid.square_subset_iff line 231
  10. lemma OAI.SharpNodal.Grid.neighborhood_mono line 244
  11. lemma OAI.SharpNodal.Grid.Cell.near_mono line 251
  12. lemma OAI.SharpNodal.Grid.Cell.div_of_mem line 256
  13. lemma OAI.SharpNodal.Grid.Cell.subset_of_intersection line 263
  14. lemma OAI.SharpNodal.Grid.Cell.subset_or_disjoint line 274
  15. lemma OAI.SharpNodal.Grid.Cell.equal_level_eq_of_intersection line 281
  16. lemma OAI.SharpNodal.Grid.square_subset_large_neighborhood line 291
  17. def OAI.SharpNodal.Grid.Cell.ancestors line 309
  18. def OAI.SharpNodal.Grid.Cell.rank line 311
  19. def OAI.SharpNodal.Grid.Cell.largerAt line 313
  20. def OAI.SharpNodal.Grid.Cell.smallerAt line 315
  21. def OAI.SharpNodal.Grid.Cell.mismatch line 317
  22. def OAI.SharpNodal.Grid.totalAt line 320
  23. lemma OAI.SharpNodal.Grid.Cell.rank_strict line 322
  24. lemma OAI.SharpNodal.Grid.Cell.same_rank_disjoint line 336
  25. lemma OAI.SharpNodal.Grid.card_le_add_symmDiff line 348
  26. lemma OAI.SharpNodal.Grid.Cell.rank_control line 357
  27. theorem OAI.SharpNodal.Grid.finite_greedy line 390
  28. lemma OAI.SharpNodal.Grid.disjoint_cover_card line 436
  29. theorem OAI.SharpNodal.Grid.rank_selection line 453
  30. def OAI.SharpNodal.Grid.expanded line 513
  31. def OAI.SharpNodal.Grid.strip line 516
  32. def OAI.SharpNodal.Grid.border line 520
  33. lemma OAI.SharpNodal.Grid.card_strip line 523
  34. lemma OAI.SharpNodal.Grid.card_border_le line 545
  35. lemma OAI.SharpNodal.Grid.mem_border_of line 550
  36. lemma OAI.SharpNodal.Grid.square_subset_expanded line 579
  37. lemma OAI.SharpNodal.Grid.Cell.mismatch_collar line 582