OAI/GroupTheory/SimpleOvergroups/SemanticDouble.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.orbit_step line 17
  2. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.orbit_surjective line 24
  3. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.P₁ line 40
  4. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.P₂ line 41
  5. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.N₁ line 42
  6. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.N₂ line 43
  7. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.C₁ line 44
  8. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.I₁ line 45
  9. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.C₂ line 46
  10. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.I₂ line 47
  11. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.GroupName line 49
  12. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.PointName line 50
  13. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.point_in_orbit line 52
  14. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.calculus line 58
  15. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.interpretation line 72
  16. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.groupKey_injective line 85
  17. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.pointKey_injective line 90
  18. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.groupValue_surjective line 97
  19. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.pointValue_base line 102
  20. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.pointValue_surjective line 108
  21. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.partialGroupKey_full line 117
  22. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticDouble.partialPointKey_full line 127