OAI/Combinatorics/KMedian/Machines/Ordered.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedian.PCP.Compiler.Ordered line 10
2. def OAI.MetricKMedian.PCP.Compiler.Ordered.equiv line 16
3. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.equiv_val line 18
4. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.length_card line 19
5. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.get_equiv line 21
6. def OAI.MetricKMedian.PCP.Compiler.Ordered.map line 23
7. def OAI.MetricKMedian.PCP.Compiler.Ordered.fin line 27
8. def OAI.MetricKMedian.PCP.Compiler.Ordered.fixed line 31
9. def OAI.MetricKMedian.PCP.Compiler.Ordered.filter line 33