OAI/Combinatorics/KMedian/Binary/BinaryAutoFiniteLists.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.Binary.Automatic.Poly.bool_any line 11
2. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_take line 12
3. theorem OAI.MetricKMedian.Binary.Automatic.Poly.list_drop line 14
4. def OAI.MetricKMedian.Binary.Automatic.Poly.natMember line 17
5. theorem OAI.MetricKMedian.Binary.Automatic.Poly.natMember_poly line 18
6. theorem OAI.MetricKMedian.Binary.Automatic.Poly.natMember_true line 22
7. theorem OAI.MetricKMedian.EncodingLists.length_filter_ofFn line 29
8. theorem OAI.MetricKMedian.EncodingLists.bool_card line 38