OAI/Combinatorics/LowSpaceSubsetSum/Counting/TopCoordinatesBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Concrete local coordinates obtained by sorting the four top blocks

  1. def OAI.LowSpaceSubsetSum.TopCoordinates.ofBlocks line 14

    Source documentation

    Mathlib's increasing finite-set enumeration is implemented by sorting; the coordinate map contains no choice of a solution subset.

    def ofBlocks (B : Fin 4 → Finset (Fin n)) (hcard : ∀ i, (B i).card = g)
    (hdisj : ∀ i j, i ≠ j → Disjoint (B i) (B j)) : TopCoordinates n g where
…

    Mentions: OAI.LowSpaceSubsetSum.TopCoordinates

  2. theorem OAI.LowSpaceSubsetSum.TopCoordinates.ofBlocks_index_mem line 36
  3. theorem OAI.LowSpaceSubsetSum.TopCoordinates.ofBlocks_index_surjective line 40
  4. theorem OAI.LowSpaceSubsetSum.TopCoordinates.ofBlocks_domain line 47
  5. theorem OAI.LowSpaceSubsetSum.TopCoordinates.ofBlocks_local_image line 59
  6. theorem OAI.LowSpaceSubsetSum.TopCoordinates.ofBlocks_local_card line 74