OAI/Combinatorics/Chromatic/Walls/IsotropicLiteralPositive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.literal_isotropic_adjoint line 16
2. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.inverse_adjoint line 76
3. theorem OAI.ElementaryPositivity.QuantumTorus.closed_isotropic_adjoint line 98
4. lemma OAI.ElementaryPositivity.QuantumTorus.inPrecisionClosure_of_cuts line 133
5. def OAI.ElementaryPositivity.QuantumTorus.positiveRayWithZero line 146
6. lemma OAI.ElementaryPositivity.QuantumTorus.positiveRayWithZero_isotropic line 157
7. lemma OAI.ElementaryPositivity.QuantumTorus.closed_ray_crossing line 166
8. theorem OAI.ElementaryPositivity.QuantumTorus.global_ray_closure line 202
9. theorem OAI.ElementaryPositivity.QuantumTorus.literal_global_positive_crossings line 212