OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarseEquivalenceMetric.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.GroupBornologous.bounded_metric_steps line 16
2. theorem OAI.PolycyclicRecognition.GroupBornologous.coarseLipschitz line 29
3. theorem OAI.PolycyclicRecognition.finite_groupDifference_bounded_error line 38
4. def OAI.PolycyclicRecognition.GroupCoarseEquivalence.metric line 49

   Source documentation

   On metrics with linear chains and finite balls, an actual discrete coarse equivalence is a metric quasi-equivalence.

   def GroupCoarseEquivalence.metric (e : GroupCoarseEquivalence G H)
       (CG : LinearMetricChains G) (CH : LinearMetricChains H)
       (hG : ∀ R : ℝ, (closedBall (1 : G) R).Finite)
       (hH : ∀ R : ℝ, (closedBall (1 : H) R).Finite) : MetricQuasiEquivalence G H where
   …

   Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.MetricQuasiEquivalence

5. def OAI.PolycyclicRecognition.MulEquiv.groupCoarseEquivalence line 61

   Source documentation

   An isomorphism is also a discrete coarse equivalence, with exact inverses.

   def MulEquiv.groupCoarseEquivalence (e : G ≃* H) : GroupCoarseEquivalence G H where
   …

   Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence