OAI/Geometry/PeriodicTiling/Model.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.Lattice line 11

    Distinct definitions of this name: ComparatorChallenges/PeriodicTilingThree.lean:11 (same statement text; different proof or body). Qualify references as OAI.PeriodicTilingThree.Lattice@path.

  2. def OAI.PeriodicTilingThree.Tiles line 17

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:15 (same declaration text).

  3. def OAI.PeriodicTilingThree.Period line 20

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:18 (same declaration text).

  4. def OAI.PeriodicTilingThree.FullyPeriodic line 23

    Distinct definitions of this name: ComparatorChallenges/PeriodicTilingThree.lean:21 (same statement text; different proof or body). Qualify references as OAI.PeriodicTilingThree.FullyPeriodic@path.

  5. abbrev OAI.PeriodicTilingThree.Space line 30

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:26 (same declaration text).

  6. def OAI.PeriodicTilingThree.castLattice line 32

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:28 (same declaration text).

  7. def OAI.PeriodicTilingThree.unitCube line 37

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:33 (same declaration text).

  8. def OAI.PeriodicTilingThree.Thickening line 39

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:35 (same declaration text).

  9. def OAI.PeriodicTilingThree.AETiles line 42

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:38 (same declaration text).

  10. def OAI.PeriodicTilingThree.latticeOfBasis line 45

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:41 (same declaration text).

  11. def OAI.PeriodicTilingThree.EuclideanFullyPeriodic line 48

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:44 (same declaration text).

  12. def OAI.PeriodicTilingThree.HasTileWithoutPeriodicComplement line 51

    Also declared: ComparatorChallenges/PeriodicTilingThree.lean:47 (same declaration text).