OAI/Geometry/Borsuk/MatrixGeometry/LineRepresentative.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.rankOne_smul line 15
2. lemma OAI.BorsukNine.rankOne_unit_span line 21
3. def OAI.BorsukNine.lineRepresentative line 29
4. def OAI.BorsukNine.HasPositiveLine line 32
5. lemma OAI.BorsukNine.lineRepresentative_norm line 36
6. lemma OAI.BorsukNine.hasPositiveLine_trace_pos line 41
7. lemma OAI.BorsukNine.positive_line_representative line 47
8. lemma OAI.BorsukNine.lineRepresentative_inner_pos line 58
9. lemma OAI.BorsukNine.lineRepresentative_continuousOn line 73
10. lemma OAI.BorsukNine.positive_line_isOpen line 84
11. lemma OAI.BorsukNine.unit_rankOne_inner_nonzero line 92