OAI/Combinatorics/KMedian/Model.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Instance line 12

    Also declared: ComparatorChallenges/KMedianThreshold.lean:9 (same declaration text), ComparatorChallenges/MetricKMedian.lean:12 (same declaration text).

  2. def OAI.MetricKMedian.encodeNat line 25

    Also declared: ComparatorChallenges/KMedianThreshold.lean:22 (same declaration text), ComparatorChallenges/MetricKMedian.lean:25 (same declaration text).

  3. def OAI.MetricKMedian.encodeRat line 28

    Also declared: ComparatorChallenges/KMedianThreshold.lean:25 (same declaration text), ComparatorChallenges/MetricKMedian.lean:28 (same declaration text).

  4. def OAI.MetricKMedian.encodeInstance line 31

    Also declared: ComparatorChallenges/KMedianThreshold.lean:28 (same declaration text), ComparatorChallenges/MetricKMedian.lean:31 (same declaration text).

  5. def OAI.MetricKMedian.nearest line 38

    Also declared: ComparatorChallenges/KMedianThreshold.lean:35 (same declaration text), ComparatorChallenges/MetricKMedian.lean:38 (same declaration text).

  6. def OAI.MetricKMedian.cost line 43

    Also declared: ComparatorChallenges/KMedianThreshold.lean:40 (same declaration text), ComparatorChallenges/MetricKMedian.lean:43 (same declaration text).

  7. def OAI.MetricKMedian.feasibleSets line 46

    Also declared: ComparatorChallenges/KMedianThreshold.lean:43 (same declaration text), ComparatorChallenges/MetricKMedian.lean:46 (same declaration text).

  8. def OAI.MetricKMedian.optimum line 49

    Also declared: ComparatorChallenges/KMedianThreshold.lean:46 (same declaration text), ComparatorChallenges/MetricKMedian.lean:49 (same declaration text).

  9. def OAI.MetricKMedian.Correct line 54

    Also declared: ComparatorChallenges/KMedianThreshold.lean:51 (same declaration text), ComparatorChallenges/MetricKMedian.lean:54 (same declaration text).