OAI/Analysis/StrictMeans/SmoothGridRegular.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrictInverseFirstPower.Grid.StarCertificate line 12
2. lemma OAI.StrictInverseFirstPower.Grid.strict_direction_bound line 18
3. lemma OAI.StrictInverseFirstPower.Grid.remainder_enlarge line 29
4. lemma OAI.StrictInverseFirstPower.Grid.strict_regular_star line 35
5. lemma OAI.StrictInverseFirstPower.Grid.compact_regular_star line 78