OAI/Combinatorics/Chromatic/Walls/InfinityLine.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.mutatedLineFactorPositive line 25
2. def OAI.ElementaryPositivity.RationalFiber.actualInfinityLineUnit line 30
3. lemma OAI.ElementaryPositivity.RationalFiber.actualInfinityLine_nocut line 34
4. lemma OAI.ElementaryPositivity.RationalFiber.actualInfinityLine_cut_unit line 104
5. lemma OAI.ElementaryPositivity.RationalFiber.line_cut_offset_ne line 138
6. lemma OAI.ElementaryPositivity.RationalFiber.line_cut_direction_ne line 149
7. lemma OAI.ElementaryPositivity.RationalFiber.actualInfinityLine_square line 155