OAI/Combinatorics/KMedianRecovery/Recovery/ImagePhaseUnion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.image_phase_union line 10
2. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.after_map line 17
3. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.History.after_subset line 25
4. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.advance_rows line 33
5. theorem OAI.MetricKMedianRecovery.PhaseHistoryTransfer.history_map line 48
6. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.paid_image line 75
7. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.free_image line 93
8. lemma OAI.MetricKMedianRecovery.PhaseHistoryTransfer.termination_map line 103
9. theorem OAI.MetricKMedianRecovery.PhaseHistoryTransfer.terminal_history_map line 114