OAI/Combinatorics/ThinTrees/Encoding/SelectionRealization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Selection realization.

  1. def OAI.CurrentKS.Realization.maskEntry line 18
  2. instance OAI.CurrentKS.Realization.poly_maskEntry line 22
  3. def OAI.CurrentKS.Realization.maskArray line 24
  4. instance OAI.CurrentKS.Realization.poly_maskArray line 27
  5. lemma OAI.CurrentKS.Realization.sorted_selected line 30
  6. lemma OAI.CurrentKS.Realization.maskArray_data line 40
  7. lemma OAI.CurrentKS.Realization.selected_sublist line 56
  8. lemma OAI.CurrentKS.Realization.listCode_sublist_le line 62
  9. lemma OAI.CurrentKS.Realization.listCode_selected_le line 67