OAI/NumberTheory/Ostmann/Tree/CellListPigeonhole.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.boundedCellLists line 13
2. theorem OAI.Ostmann.mem_boundedCellLists line 18
3. theorem OAI.Ostmann.boundedCellLists_nonempty line 26
4. theorem OAI.Ostmann.boundedCellLists_card_le line 29
5. theorem OAI.Ostmann.common_cell_list line 49

   Source documentation

   Simultaneously fixing all list lengths and ordered cell labels costs at most the explicit finite number of bounded lists.

   theorem common_cell_list (E : Finset ℕ) (N B : ℕ) (w : ℕ → List ℕ)
       (hlen : ∀ a ∈ E, (w a).length ≤ N)
       (hentry : ∀ a ∈ E, ∀ h ∈ w a, h ≤ B) :
       ∃ v : List ℕ, ∃ S : Finset ℕ, S ⊆ E ∧
         E.card ≤ ((N + 1) * (B + 1) ^ N) * S.card ∧ ∀ a ∈ S, w a = v := by
   …