OAI/Geometry/Arnold/Quotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ArnoldCounterexample.Quadric.project_eq_iff_phase line 13
2. def OAI.ArnoldCounterexample.Quadric.unitRepresentative line 28
3. lemma OAI.ArnoldCounterexample.Quadric.project_unitRepresentative line 29
4. lemma OAI.ArnoldCounterexample.Quadric.phase_map_respects line 32
5. def OAI.ArnoldCounterexample.Quadric.descend line 41

   Source documentation

   Descent through the actual circle quotient, proved from its actual fibers.

   def descend (F : CV → CV) (hF : ∀ z : UnitQuadric, IsUnitQuadric (F z)) (q : Q3) : Q3 :=
   …

   Mentions: OAI.ArnoldCounterexample.CV, OAI.ArnoldCounterexample.UnitQuadric, OAI.ArnoldCounterexample.IsUnitQuadric, OAI.ArnoldCounterexample.Q3

6. lemma OAI.ArnoldCounterexample.Quadric.descend_project line 44
7. def OAI.ArnoldCounterexample.Quadric.descendEquiv line 49