OAI/MeasureTheory/Falconer/Angular/GnomonicDischarge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The published gnomonic surface identity proved from Euclidean cone volume

  1. theorem OAI.Falconer.gnomonic_sphere_image line 10
  2. theorem OAI.Falconer.published_gnomonic_surface line 28