OAI/Combinatorics/UniformKServer/TreeLeaves.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Unique child on a leaf path and conservation of literal hidden counts.

  1. def OAI.UniformKServer.TreeLeaves.leaf line 16
  2. theorem OAI.UniformKServer.TreeLeaves.root_descends line 18
  3. theorem OAI.UniformKServer.TreeLeaves.child_path line 25
  4. def OAI.UniformKServer.TreeLeaves.indicator line 36
  5. theorem OAI.UniformKServer.TreeLeaves.indicator_root line 38
  6. theorem OAI.UniformKServer.TreeLeaves.indicator_children line 40
  7. def OAI.UniformKServer.TreeLeaves.count line 56
  8. theorem OAI.UniformKServer.TreeLeaves.count_le line 58
  9. theorem OAI.UniformKServer.TreeLeaves.count_root line 63
  10. theorem OAI.UniformKServer.TreeLeaves.count_children line 66