OAI/Analysis/SymmetricDomains/CompactPeakRatio.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.RelationSteps.trans line 18
  2. theorem OAI.Release061.RelationSteps.single line 28
  3. theorem OAI.Release061.compact_connected_relation_chains line 31
  4. theorem OAI.Release061.IsSmooth.discRelation_nhds line 58
  5. theorem OAI.Release061.disc_peak_ratio line 83
  6. theorem OAI.Release061.DiscRelation.entire_peak_ratio line 124
  7. theorem OAI.Release061.RelationSteps.symm line 133
  8. theorem OAI.Release061.RelationSteps.map line 144
  9. theorem OAI.Release061.RelationSteps.ratio line 154
  10. theorem OAI.Release061.IsSmooth.compact_disc_chains line 175
  11. theorem OAI.Release061.IsSmooth.compact_peak_ratio line 188