OAI/Analysis/SymmetricDomains/ModelChartOpen.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.supportLinearCoordinates line 36
2. lemma OAI.Release061.supportLinearCoordinates_fst line 40
3. lemma OAI.Release061.supportLinearCoordinates_im line 44
4. def OAI.Release061.modelBoundedChart line 50
5. lemma OAI.Release061.modelBoundedChart_apply line 54
6. lemma OAI.Release061.modelBoundedChart_analytic line 58
7. lemma OAI.Release061.modelBoundedChart_inverse_analytic line 65
8. theorem OAI.Release061.modelBoundedChart_bounded_open line 73