OAI/MathematicalPhysics/PEPSSubvolume/Pinning.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Pinned core/shell tensor coordinates and isometric insertion.

  1. def OAI.PolynomialPEPS.Subvolume.Pinning.coreRestrict line 25
  2. def OAI.PolynomialPEPS.Subvolume.Pinning.shellRestrict line 28
  3. def OAI.PolynomialPEPS.Subvolume.Pinning.joinWithin line 31
  4. theorem OAI.PolynomialPEPS.Subvolume.Pinning.core_joinWithin line 35
  5. theorem OAI.PolynomialPEPS.Subvolume.Pinning.shell_joinWithin line 41
  6. theorem OAI.PolynomialPEPS.Subvolume.Pinning.joinWithin_restrict line 47
  7. def OAI.PolynomialPEPS.Subvolume.Pinning.splitEquiv line 53
  8. def OAI.PolynomialPEPS.Subvolume.Pinning.insertion line 60
  9. theorem OAI.PolynomialPEPS.Subvolume.Pinning.insertion_join line 64
  10. theorem OAI.PolynomialPEPS.Subvolume.Pinning.insertion_isometry line 69
  11. theorem OAI.PolynomialPEPS.Subvolume.Pinning.liftBetween_core_join line 85
  12. theorem OAI.PolynomialPEPS.Subvolume.Pinning.liftBetween_shell_join line 106