OAI/Combinatorics/IndependentSets/Geometry/PatternInvariant.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.PatternInvariant line 10
  2. lemma OAI.LargeIndependentSets.occupied_measurable line 13
  3. theorem OAI.LargeIndependentSets.invariant_pattern_cut_in_list line 17
  4. def OAI.LargeIndependentSets.GloballyAligned line 59
  5. theorem OAI.LargeIndependentSets.invariant_pattern_globally_aligned line 62
  6. def OAI.LargeIndependentSets.GoodPatternOn line 85
  7. lemma OAI.LargeIndependentSets.GloballyAligned.goodOn line 90
  8. theorem OAI.LargeIndependentSets.invariant_pattern_no_bad_sets line 96
  9. def OAI.LargeIndependentSets.ListIndex.inside line 103
  10. lemma OAI.LargeIndependentSets.ListIndex.map_inside line 112
  11. def OAI.LargeIndependentSets.ListSlot.inside line 119
  12. lemma OAI.LargeIndependentSets.ListSlot.map_inside line 123
  13. def OAI.LargeIndependentSets.liftData line 128
  14. lemma OAI.LargeIndependentSets.liftData_true_iff line 134
  15. def OAI.LargeIndependentSets.ListPattern.lift line 142
  16. lemma OAI.LargeIndependentSets.ListSlot.inside_map line 169
  17. lemma OAI.LargeIndependentSets.ListPattern.restrict_lift line 176
  18. lemma OAI.LargeIndependentSets.ListIndex.map_id line 191
  19. lemma OAI.LargeIndependentSets.ListSlot.map_id line 196
  20. lemma OAI.LargeIndependentSets.ListSlot.map_comp line 200
  21. lemma OAI.LargeIndependentSets.ListPattern.restrict_id line 208
  22. lemma OAI.LargeIndependentSets.ListPattern.restrict_comp line 216
  23. def OAI.LargeIndependentSets.ListPattern.extendFin line 227
  24. lemma OAI.LargeIndependentSets.ListPattern.restrict_extendFin line 231
  25. lemma OAI.LargeIndependentSets.GloballyAligned.good_full_restrict line 242
  26. lemma OAI.LargeIndependentSets.isClopen_finite_pattern_event line 255
  27. lemma OAI.LargeIndependentSets.isClopen_bad_restrict line 258
  28. lemma OAI.LargeIndependentSets.ListPattern.measurable_restrict line 264
  29. def OAI.LargeIndependentSets.restrictionLaw line 275
  30. lemma OAI.LargeIndependentSets.restrictionLaw_comp line 280
  31. lemma OAI.LargeIndependentSets.restrictionLaw_id line 291
  32. lemma OAI.LargeIndependentSets.finite_laws_invariant line 300
  33. instance OAI.LargeIndependentSets.patternMetrizable line 364
  34. instance OAI.LargeIndependentSets.patternSecondCountable line 369
  35. instance OAI.LargeIndependentSets.finitePatternLawMetric line 374
  36. lemma OAI.LargeIndependentSets.continuous_restrictionLaw line 380
  37. theorem OAI.LargeIndependentSets.no_asymptotically_invariant_bad_sequence line 384