OAI/Geometry/SmoothYau/ProductMetric/SphereProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.four_nodal_finite line 10
2. lemma OAI.YauCounterexamples.four_sign_nodal_real line 24
3. lemma OAI.YauCounterexamples.four_witnesses_unbounded line 37
4. theorem OAI.YauCounterexamples.sphere_two_torus_two line 75

   Distinct definitions of this name: ComparatorChallenges/SmoothYau.lean:139 (same statement text; different proof or body). Qualify references as OAI.YauCounterexamples.sphere_two_torus_two@path.