OAI/Geometry/PlaneColoring/FourContinuity.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.four_avoiding_traces line 9
  2. lemma OAI.EuclideanFiveColor.four_state_trace_domination line 27
  3. def OAI.EuclideanFiveColor.indL2 line 73
  4. lemma OAI.EuclideanFiveColor.indL2_ae line 75
  5. lemma OAI.EuclideanFiveColor.indL2_nonneg line 77
  6. lemma OAI.EuclideanFiveColor.indL2_le_one line 81
  7. lemma OAI.EuclideanFiveColor.indL2_norm line 85
  8. lemma OAI.EuclideanFiveColor.indL2_sum line 90
  9. lemma OAI.EuclideanFiveColor.weak_limit_le line 99
  10. lemma OAI.EuclideanFiveColor.indL2_weak_L1 line 109
  11. def OAI.EuclideanFiveColor.fourStateL2 line 149
  12. lemma OAI.EuclideanFiveColor.four_weak_limit_identify line 151
  13. def OAI.EuclideanFiveColor.fourStateDistance line 223
  14. lemma OAI.EuclideanFiveColor.four_state_subseq_continuity line 226
  15. lemma OAI.EuclideanFiveColor.four_state_continuity line 248
  16. lemma OAI.EuclideanFiveColor.angleMk_compact_bound line 268
  17. lemma OAI.EuclideanFiveColor.angular_compact_L1 line 296
  18. lemma OAI.EuclideanFiveColor.support_lower_semicontinuity line 311
  19. lemma OAI.EuclideanFiveColor.support_sequence_continuity line 336
  20. lemma OAI.EuclideanFiveColor.strict_state_uniform_on_compact line 361
  21. lemma OAI.EuclideanFiveColor.angle_preimage_positive line 407
  22. def OAI.EuclideanFiveColor.fourRealState line 414
  23. def OAI.EuclideanFiveColor.fourSupport line 415
  24. lemma OAI.EuclideanFiveColor.four_realState_measurable line 416
  25. lemma OAI.EuclideanFiveColor.four_realState_positive line 419
  26. lemma OAI.EuclideanFiveColor.four_realState_continuity line 423
  27. lemma OAI.EuclideanFiveColor.four_support_continuity line 432
  28. lemma OAI.EuclideanFiveColor.four_support_sequence_no_unit line 441
  29. lemma OAI.EuclideanFiveColor.plane_antilipschitz_qmp line 465
  30. lemma OAI.EuclideanFiveColor.support_prod_real line 472
  31. lemma OAI.EuclideanFiveColor.continuousAt_maps_support_closed line 481
  32. lemma OAI.EuclideanFiveColor.state_support_transport line 488