OAI/NumberTheory/Ostmann/Construction/IntegerCenterSelection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.exists_pair_avoiding_bad line 8
2. def OAI.Ostmann.Construction.integerCenterWindow line 32
3. lemma OAI.Ostmann.Construction.mem_integerCenterWindow line 34
4. lemma OAI.Ostmann.Construction.integerCenterWindow_card_lower line 39
5. theorem OAI.Ostmann.Construction.exists_pair_integer_centers line 52
6. theorem OAI.Ostmann.Construction.exists_triple_integer_centers line 68