OAI/Combinatorics/KMedianRecovery/Recovery/SwapOriginal.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedianRecovery.FreshLeafTransfer.swap_originalline 11 - lemma
OAI.MetricKMedianRecovery.FreshLeafTransfer.image_originalline 17 - lemma
OAI.MetricKMedianRecovery.FreshLeafTransfer.image_copyline 26 - lemma
OAI.MetricKMedianRecovery.FreshLeafTransfer.shorteningline 33 - theorem
OAI.MetricKMedianRecovery.FreshLeafTransfer.terminal_transferline 53