OAI/Analysis/AffineBernstein/FlatProductCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.flatProductCoordinates line 16
2. def OAI.AffineBernstein.flatProductFiberBasis line 21
3. def OAI.AffineBernstein.flatProductEmbedding line 25
4. lemma OAI.AffineBernstein.flatProductEmbedding_apply line 31
5. lemma OAI.AffineBernstein.flatProductFiberBasis_last line 34
6. lemma OAI.AffineBernstein.flatProductFiberBasis_first line 39
7. lemma OAI.AffineBernstein.flatProductEmbedding_injective line 44
8. lemma OAI.AffineBernstein.flatProductEmbedding_vertical line 51
9. lemma OAI.AffineBernstein.flatProductCoordinates_basis line 57
10. lemma OAI.AffineBernstein.flatProductEmbedding_affine line 67
11. lemma OAI.AffineBernstein.flatProductCoordinates_measurePreserving line 79