OAI/Combinatorics/Chromatic/Walls/ComparisonRefinement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ElementaryPositivity.RationalFiber.CrossingClose line 19
2. lemma OAI.ElementaryPositivity.RationalFiber.CrossingClose.action line 26
3. lemma OAI.ElementaryPositivity.RationalFiber.bounded_action_trivial line 38
4. inductive OAI.ElementaryPositivity.RationalFiber.WordRefines line 50
5. lemma OAI.ElementaryPositivity.RationalFiber.WordRefines.action line 59
6. inductive OAI.ElementaryPositivity.RationalFiber.CrossingTrivial line 89
7. lemma OAI.ElementaryPositivity.RationalFiber.CrossingTrivial.mono line 95
8. lemma OAI.ElementaryPositivity.RationalFiber.CrossingClose.refl line 101
9. def OAI.ElementaryPositivity.RationalFiber.orientedBounded line 107
10. lemma OAI.ElementaryPositivity.RationalFiber.orientedBounded_trivial line 112
11. lemma OAI.ElementaryPositivity.RationalFiber.CrossingTrivial.insert line 120
12. lemma OAI.ElementaryPositivity.RationalFiber.filter_word_refines line 128