OAI/Analysis/SymmetricDomains/SemialgebraicOffsetLimitsFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.SignElimination.polynomialSignSet_bounded_inward_selection line 37
2. theorem OAI.Release061.isSemialgebraic_iff_polynomialSignSet line 81
3. lemma OAI.Release061.real_polynomial_zero_null line 97
4. lemma OAI.Release061.PolynomialSignSet.parameter_strip line 112
5. theorem OAI.Release061.semialgebraic_boundary_fiber_closure_from_family line 130
6. theorem OAI.Release061.semialgebraic_bounded_selection_from_family line 164
7. theorem OAI.Release061.semialgebraic_inward_analytic_from_family line 196
8. theorem OAI.Release061.semialgebraic_offset_limits_from_family line 225