OAI/GroupTheory/FiniteType/TwistedBrinBasisTranslateEquiv.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwistedBrin.Basis.translateEquiv line 20
  2. lemma OAI.TwistedBrin.Basis.translateEquiv_val line 33
  3. lemma OAI.TwistedBrin.Basis.translate_chart_gauge line 36
  4. lemma OAI.TwistedBrin.Basis.translate_cutRefines line 47
  5. def OAI.TwistedBrin.Prefix.splitEquiv line 83
  6. lemma OAI.TwistedBrin.Prefix.splitEquiv_apply line 93
  7. def OAI.TwistedBrin.LocalEmbedding.glueTwo line 103
  8. lemma OAI.TwistedBrin.LocalEmbedding.glueTwo_chart line 127
  9. lemma OAI.TwistedBrin.LocalEmbedding.glueTwo_comp line 134
  10. lemma OAI.TwistedBrin.LocalEmbedding.range_glueTwo line 140
  11. def OAI.TwistedBrin.Basis.chartPartitionEquiv line 158
  12. lemma OAI.TwistedBrin.Basis.chartPartitionEquiv_val line 172
  13. lemma OAI.TwistedBrin.Basis.cutRefines_ofChartPartition line 176
  14. lemma OAI.TwistedBrin.Basis.chart_germ line 213
  15. lemma OAI.TwistedBrin.Basis.regions_disjoint line 216
  16. structure OAI.TwistedBrin.Basis.Merge line 222
  17. def OAI.TwistedBrin.Basis.Merge.ofPair line 236
  18. lemma OAI.TwistedBrin.Basis.Merge.range_joined line 251
  19. abbrev OAI.TwistedBrin.Basis.Merge.Rest line 284
  20. abbrev OAI.TwistedBrin.Basis.Merge.Roots line 285
  21. def OAI.TwistedBrin.Basis.Merge.leafEquiv line 287
  22. def OAI.TwistedBrin.Basis.Merge.rootChart line 316
  23. lemma OAI.TwistedBrin.Basis.Merge.rootPartition line 320
  24. def OAI.TwistedBrin.Basis.Merge.lower line 356
  25. lemma OAI.TwistedBrin.Basis.Merge.rank_lower line 360
  26. lemma OAI.TwistedBrin.Basis.Merge.lower_cutRefines line 369
  27. lemma OAI.TwistedBrin.Basis.Merge.lower_ne line 387
  28. lemma OAI.TwistedBrin.Pattern.graft_leaf line 400
  29. def OAI.TwistedBrin.Pattern.insert line 405
  30. lemma OAI.TwistedBrin.Pattern.insert_leaf line 409
  31. lemma OAI.TwistedBrin.Pattern.insert_left line 413
  32. lemma OAI.TwistedBrin.Pattern.insert_right line 418
  33. lemma OAI.TwistedBrin.Pattern.exists_prune line 423
  34. lemma OAI.TwistedBrin.Basis.Merge.germ_mem_lower_iff line 446
  35. lemma OAI.TwistedBrin.Basis.Merge.joined_ne_piece line 468
  36. def OAI.TwistedBrin.Basis.Merge.toLower line 479
  37. lemma OAI.TwistedBrin.Basis.Merge.toLower_val line 483
  38. def OAI.TwistedBrin.Basis.Merge.Disjoint line 485
  39. lemma OAI.TwistedBrin.Basis.Merge.disjoint_symm line 488
  40. def OAI.TwistedBrin.Basis.Merge.lift line 491
  41. lemma OAI.TwistedBrin.Basis.Merge.lower_lift_comm line 504
  42. lemma OAI.TwistedBrin.Basis.Merge.common_lower_of_disjoint line 524