OAI/GroupTheory/PolycyclicRecognition/Lattices/LatticeMetricChains.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.IsUniformLattice.nonempty_linearMetricChains line 18

   Source documentation

   Rounding an ambient chain to a uniformly close lattice section keeps the linear length bound and enlarges only the step size.

   theorem IsUniformLattice.nonempty_linearMetricChains
       (hΛ : IsUniformLattice Λ) (C : LinearMetricChains G) :
       Nonempty (LinearMetricChains Λ) := by
   …

2. theorem OAI.PolycyclicRecognition.IsUniformLattice.nonempty_metricQuasiEquivalence line 53

   Source documentation

   Inclusion and a bounded section are metric quasi-inverses.

   theorem IsUniformLattice.nonempty_metricQuasiEquivalence
       (hΛ : IsUniformLattice Λ) : Nonempty (MetricQuasiEquivalence Λ G) := by
   …

   Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence