OAI/Analysis/SymmetricDomains/NormalOffsetFamilyJoint.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.SignElimination.polynomialSignSet_preimage_of_graph line 34
2. lemma OAI.Release061.PolynomialSignSet.closure line 56
3. lemma OAI.Release061.PolynomialSignSet.interior line 78
4. lemma OAI.Release061.PolynomialSignSet.frontier line 82
5. def OAI.Release061.normalOffsetFamily line 92
6. lemma OAI.Release061.normalOffsetFamily_polynomialSignSet line 97
7. lemma OAI.Release061.normalOffsetFamily_isOpen line 134
8. lemma OAI.Release061.normalOffsetFamily_zero_not_mem line 147
9. lemma OAI.Release061.normalOffsetFamily_joint_closure line 154