OAI/Combinatorics/ThinTrees/Continuation/PartitionResponse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Partition response.

  1. lemma OAI.AlgorithmicThinTrees.Partitions.lift_restrict_crossing line 18
  2. lemma OAI.AlgorithmicThinTrees.Partitions.restrict_crossing_card line 29
  3. lemma OAI.AlgorithmicThinTrees.Partitions.lift_restrict_crossing_filter line 33
  4. lemma OAI.AlgorithmicThinTrees.Partitions.restrict_bad_card line 40
  5. theorem OAI.AlgorithmicThinTrees.Partitions.finite_chain_response line 48