OAI/Combinatorics/ThinTrees/Metric/AssignedGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Metric assigned geometry.

  1. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normDistance_nonneg line 18
  2. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normDistance_reverse line 21
  3. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.profile_shell_edge_bound line 26
  4. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.profile_radial_max line 44
  5. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.profile_radial_move line 56
  6. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.ball_meets_radial line 80