OAI/Combinatorics/KMedian/Process/FiniteGraph.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedian.FiniteGraph.incomingline 11 - def
OAI.MetricKMedian.FiniteGraph.touchingline 14 - theorem
OAI.MetricKMedian.FiniteGraph.mem_touchingline 17 - theorem
OAI.MetricKMedian.FiniteGraph.touching_cardline 22 - def
OAI.MetricKMedian.FiniteGraph.conflictsline 30 - theorem
OAI.MetricKMedian.FiniteGraph.self_not_conflictline 33 - theorem
OAI.MetricKMedian.FiniteGraph.conflicts_cardline 36 - theorem
OAI.MetricKMedian.FiniteGraph.relevant_cardline 47