OAI/GroupTheory/FiniteType/TwistedBrinBasisGroundMatching.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwistedBrin.Basis.groundMatching line 22
  2. def OAI.TwistedBrin.Basis.Matching.available line 41
  3. lemma OAI.TwistedBrin.Basis.Matching.mem_available line 45
  4. lemma OAI.TwistedBrin.Basis.Matching.available_present line 50
  5. lemma OAI.TwistedBrin.Basis.Matching.available_mono line 53
  6. lemma OAI.TwistedBrin.Basis.Matching.available_subset line 59
  7. lemma OAI.TwistedBrin.Basis.Matching.unavailable_bound line 62
  8. lemma OAI.TwistedBrin.Basis.Matching.available_nonempty line 85
  9. structure OAI.TwistedBrin.Basis.CutDown line 97
  10. lemma OAI.TwistedBrin.Basis.CutDown.ext line 103
  11. instance OAI.TwistedBrin.Basis.CutDown.(instance at line 105) line 105
  12. lemma OAI.TwistedBrin.Basis.CutDown.rank_lt_top line 110
  13. lemma OAI.TwistedBrin.Basis.CutDown.strictMono_rank line 112
  14. def OAI.TwistedBrin.Basis.CutDown.upperInterval line 117
  15. abbrev OAI.TwistedBrin.Basis.CutDown.Near line 127
  16. def OAI.TwistedBrin.Basis.CutDown.nearInclude line 128
  17. structure OAI.TwistedBrin.Basis.Matching.Pair line 135
  18. lemma OAI.TwistedBrin.Basis.Matching.Pair.ext line 144
  19. instance OAI.TwistedBrin.Basis.Matching.Pair.(instance at line 146) line 146
  20. def OAI.TwistedBrin.Basis.Matching.projectPair line 153
  21. def OAI.TwistedBrin.Basis.Matching.contractPair line 155
  22. lemma OAI.TwistedBrin.Basis.Matching.contractPair_le_base line 168
  23. abbrev OAI.TwistedBrin.Basis.Matching.GroundFaces line 171
  24. def OAI.TwistedBrin.Basis.Matching.ground line 173
  25. def OAI.TwistedBrin.Basis.Matching.selectedPair line 184
  26. lemma OAI.TwistedBrin.Basis.Matching.contractPair_le_ground line 187
  27. abbrev OAI.TwistedBrin.Basis.Matching.AvailableFaces line 191
  28. def OAI.TwistedBrin.Basis.Matching.fiberResolution line 194
  29. def OAI.TwistedBrin.Basis.Matching.fiberInclusion line 202
  30. lemma OAI.TwistedBrin.Basis.Matching.fiber_comparison line 207
  31. lemma OAI.TwistedBrin.Basis.Matching.fiber_exactIn line 220
  32. lemma OAI.TwistedBrin.Basis.Matching.fiber_nonempty line 230
  33. lemma OAI.TwistedBrin.Basis.Matching.ground_exactIn line 235
  34. theorem OAI.TwistedBrin.Basis.Matching.near_nullIn line 241
  35. lemma OAI.TwistedBrin.Basis.CutDown.upper_nonempty line 291
  36. theorem OAI.TwistedBrin.Basis.CutDown.exactIn_high_rank line 302
  37. structure OAI.TwistedBrin.Basis.CutBasis line 386
  38. lemma OAI.TwistedBrin.Basis.CutBasis.ext line 389
  39. instance OAI.TwistedBrin.Basis.CutBasis.(instance at line 391) line 391
  40. instance OAI.TwistedBrin.Basis.CutBasis.(instance at line 392) line 392
  41. lemma OAI.TwistedBrin.Basis.CutBasis.strictMono_rank line 397
  42. lemma OAI.TwistedBrin.Basis.CutBasis.directed line 401
  43. def OAI.TwistedBrin.Basis.CutBasis.lowerEquiv line 404
  44. lemma OAI.TwistedBrin.Basis.CutBasis.lower_nonempty line 411
  45. lemma OAI.TwistedBrin.Basis.CutBasis.lower_exactSet line 416
  46. theorem OAI.TwistedBrin.Basis.CutBasis.sublevel_exact line 423