OAI/Geometry/PeriodicTiling/BlockActivationInverse.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PeriodicTilingThree.BlockShiftData line 11
  2. def OAI.PeriodicTilingThree.BlockShiftData.ofMultiplicity line 22
  3. def OAI.PeriodicTilingThree.BlockShiftData.blockForward line 34
  4. def OAI.PeriodicTilingThree.BlockShiftData.blockInverse line 39
  5. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverse_inl line 49
  6. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverse_inr line 56
  7. theorem OAI.PeriodicTilingThree.BlockShiftData.blockForward_inl line 63
  8. theorem OAI.PeriodicTilingThree.BlockShiftData.blockForward_inr line 72
  9. theorem OAI.PeriodicTilingThree.BlockShiftData.recoverA line 81
  10. theorem OAI.PeriodicTilingThree.BlockShiftData.recoverB line 90
  11. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverse_forward_inl line 99
  12. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverse_forward_inr line 110
  13. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverse_forward line 121
  14. theorem OAI.PeriodicTilingThree.BlockShiftData.blockForward_inverse_inl line 140
  15. theorem OAI.PeriodicTilingThree.BlockShiftData.blockForward_inverse_inr line 165
  16. theorem OAI.PeriodicTilingThree.BlockShiftData.blockForward_inverse line 190
  17. def OAI.PeriodicTilingThree.BlockShiftData.blockInverseEquiv line 209
  18. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverseEquiv_apply line 218
  19. theorem OAI.PeriodicTilingThree.BlockShiftData.blockInverseEquiv_symm_apply line 225