OAI/Combinatorics/KMedianRecovery/Strictness/OpenableMap.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedianRecovery.PhaseParameterTransfer.openable_mapline 12 - lemma
OAI.MetricKMedianRecovery.PhaseParameterTransfer.image_regular_unionline 39 - theorem
OAI.MetricKMedianRecovery.PhaseParameterTransfer.prefix_mapline 47 - theorem
OAI.MetricKMedianRecovery.PhaseParameterTransfer.valid_mapline 76