OAI/Combinatorics/KMedian/Process/PhysicalRound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.CopyState.forcedGroups line 14
2. def OAI.MetricKMedian.CopyState.forcedAlive line 17
3. theorem OAI.MetricKMedian.CopyState.forcedAlive_subset line 21
4. theorem OAI.MetricKMedian.CopyState.heavy_alive_forced line 25
5. def OAI.MetricKMedian.CopyState.roundAlive line 31
6. theorem OAI.MetricKMedian.CopyState.nextAliveAt_subset_physical line 37
7. theorem OAI.MetricKMedian.CopyState.roundAlive_subset line 46
8. theorem OAI.MetricKMedian.CopyState.roundAlive_active line 55
9. theorem OAI.MetricKMedian.CopyState.roundAlive_not_reset line 70
10. theorem OAI.MetricKMedian.CopyState.round_cap line 98