OAI/Combinatorics/Chromatic/Walls/FinitePathPerturbation.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.FiniteRayGeometry.preserve_finite_affine_signsline 11 - lemma
OAI.ElementaryPositivity.FiniteRayGeometry.exists_generic_offset_with_probesline 29 - lemma
OAI.ElementaryPositivity.FiniteRayGeometry.affine_event_betweenline 57 - lemma
OAI.ElementaryPositivity.FiniteRayGeometry.perturbed_event_betweenline 64 - lemma
OAI.ElementaryPositivity.FiniteRayGeometry.dense_annihilator_avoidline 81 - lemma
OAI.ElementaryPositivity.FiniteRayGeometry.countable_avoid_with_probesline 100 - lemma
OAI.ElementaryPositivity.FiniteRayGeometry.exists_all_generic_offsets_with_probesline 141