OAI/Combinatorics/KMedian/Expanders/CloudSpec.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.C line 14
2. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.VO line 15
3. abbrev OAI.MetricKMedian.PCP.Compiler.CloudSpec.EO line 16
4. def OAI.MetricKMedian.PCP.Compiler.CloudSpec.dartCode line 17
5. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.dartCode_injective line 18
6. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.finRange_val line 23
7. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.darts_eq line 28
8. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.endpoint_eq line 33
9. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.incident_eq line 39
10. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.active_test line 48
11. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.active_eq line 59
12. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.fin_equiv_val line 71
13. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.cloud_table line 76
14. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.cloud_length line 89
15. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.nodeCode_eq line 92
16. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.nodes_eq line 98
17. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.index_eq line 110
18. lemma OAI.MetricKMedian.PCP.Compiler.CloudSpec.global_table line 118