OAI/Geometry/Borsuk/Projectors/Tangent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.tangentPart line 12
2. lemma OAI.BorsukNine.tangentPart_add line 14
3. lemma OAI.BorsukNine.tangentPart_smul line 18
4. lemma OAI.BorsukNine.tangentPart_self line 21
5. lemma OAI.BorsukNine.tangentPart_sq line 24
6. lemma OAI.BorsukNine.tangentPart_norm_le line 32
7. lemma OAI.BorsukNine.dist_le_two_tangent line 36
8. lemma OAI.BorsukNine.tangentPart_sub line 49
9. lemma OAI.BorsukNine.tangentPart_zero line 54
10. lemma OAI.BorsukNine.tangentPart_equiv_bound line 56
11. lemma OAI.BorsukNine.spherical_local_linear_interpolation line 68