OAI/Combinatorics/SumProduct/Alignment/FiniteCover01.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FactorProgression.cell_smooth_bound line 27
2. theorem OAI.FactorProgression.factor_progression_obstruction line 49
3. def OAI.FiniteCoverObservable.translated line 150
4. lemma OAI.FiniteCoverObservable.continuous_translated line 154
5. theorem OAI.FiniteCoverObservable.compact_translated_family line 163
6. lemma OAI.FiniteCoverObservable.integral_translated line 175
7. theorem OAI.FiniteCoverObservable.finite_cover_tests line 186
8. theorem OAI.CompactFamilyDescent.finite_unit_lipschitz_obstruction line 220