OAI/Geometry/PeriodicTiling/BoundedDifferences.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PeriodicTilingThree.configDiff_boundedline 14 - theorem
OAI.PeriodicTilingThree.configDiff_eq_zero_of_secondline 25 - theorem
OAI.PeriodicTilingThree.configDiff_eq_zero_of_iterateline 64 - theorem
OAI.PeriodicTilingThree.periodic_of_bounded_configDiff_iterateline 82 - theorem
OAI.PeriodicTilingThree.forwardDiff_eq_configDiffline 88 - theorem
OAI.PeriodicTilingThree.forwardDiff_eq_zero_of_bounded_iterateline 91