OAI/RepresentationTheory/UniversalSquare/Support/SupportTransport.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Support Transport.

  1. def OAI.Saxl.SupportLE line 15
  2. lemma OAI.Saxl.SupportLE.refl line 26
  3. lemma OAI.Saxl.SupportLE.trans line 30
  4. lemma OAI.Saxl.SupportLE.of_injective line 36
  5. lemma OAI.Saxl.SupportLE.detects_map line 41
  6. lemma OAI.Saxl.SupportLE.restrict line 53
  7. lemma OAI.Saxl.SupportLE.coind line 58
  8. def OAI.Saxl.outer line 73
  9. def OAI.Saxl.outerMap line 81
  10. def OAI.Saxl.rightSlice line 94
  11. lemma OAI.Saxl.rightSlice_tmul line 98
  12. lemma OAI.Saxl.rightSlice_map line 102
  13. lemma OAI.Saxl.exists_rightSlice line 112
  14. theorem OAI.Saxl.SupportLE.outer line 128
  15. def OAI.Saxl.coindLift line 168
  16. def OAI.Saxl.coindEval line 188
  17. lemma OAI.Saxl.coindEval_lift line 205
  18. lemma OAI.Saxl.coindLift_eval line 215
  19. lemma OAI.Saxl.coindLift_ne_zero line 230
  20. lemma OAI.Saxl.coindEval_ne_zero line 240
  21. theorem OAI.Saxl.word_supportLE line 251
  22. theorem OAI.Saxl.word_coind_supportLE line 257