OAI/Analysis/SymmetricDomains/IndependentConormals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.original_boundary_positive_fiber line 36
2. def OAI.Release061.affineMapCodRestrict line 76
3. def OAI.Release061.ActualCriticalChart.fiberAffine line 92
4. lemma OAI.Release061.ActualCriticalChart.fiberAffine_apply line 97
5. def OAI.Release061.ActualCriticalChart.ambientCovector line 100
6. lemma OAI.Release061.ActualCriticalChart.ambientCovector_apply line 107
7. lemma OAI.Release061.ActualCriticalChart.ambientCovector_comp line 111
8. lemma OAI.Release061.ActualCriticalChart.ambientCovector_range line 129
9. theorem OAI.Release061.ActualCriticalChart.independent_conormals line 167