Choosing a finset of minimum cardinality

Stream: Is there code for X?

[Oliver Nash]

I have a non-empty collection of finite subsets and would like to select one of minimum cardinality. After a bit of poking around I see that I can achieve this using well_founded.min as follows:

import data.finset

namespace finset

variables {α : Type*}

-- Optional convenience definition.
def well_founded_card : well_founded (λ (s t : finset α), s.card < t.card) :=
measure_wf finset.card

variables (s : set (finset α)) (hs : s.nonempty)

noncomputable def min_card_of_nonempty : finset α :=
well_founded.min well_founded_card s hs

lemma min_card_of_nonempty_mem : min_card_of_nonempty s hs ∈ s :=
well_founded.min_mem _ _ _

lemma min_card_of_nonempty_le {t : finset α} (ht : t ∈ s) :
  (min_card_of_nonempty s hs).card ≤ t.card :=
by { rw ← not_lt, exact well_founded.not_lt_min well_founded_card s hs ht, }

end finset

[Oliver Nash]

Evidently this is a thin wrapper around well_founded.min specialising it to a very specific situation.

[Oliver Nash]

However I think this situation is important enough to be worth the specialisation: not being all that familiar with the relevant corners of the library, it took me a while to construct the above.

[Oliver Nash]

I would appreciate feedback on:

1. Am I doing this right? I'm a bit surprised we don't have an established pattern for exactly this situation already.
2. Should I PR this?

[Scott Morrison]

It seems easier to just use well_founded.min on finset.card '' s, and then take a preimage. Hopefully you can do without having to write many new lemmas that way. But I haven't looked closely.

[Oliver Nash]

Thanks!

[Oliver Nash]

I actually started with this and then thought "Surely Mathlib should be helping more than this, people _often_ want to do exactly what I'm doing?" But I wasn't confident enough in this to actually make a PR.

[Scott Morrison]

I sort of doubt exactly what you're doing is common. Taking the minimum w.r.t some function to nat (e.g. finset.card in your case) is certainly common, and perhaps could use more API. But not specifically for finset.card, I think.

[Oliver Nash]

Ah that's a good point.

[Oliver Nash]

(deleted)

[Yakov Pechersky]

Is it possible to do this by taking the first element of the list you get when you sort your finset of finsets by card? Basically, argmin

[Yakov Pechersky]

docs#list.argmin

[Yakov Pechersky]

Ah, you have an unbounded collection as a set

[Floris van Doorn]

As another data point: A while back I was also disappointed that mathlib didn't have a way of taking a minimum/making w.r.t. a function.
My preferred API for that purpose was to have a minimum/maximum that takes a set and a function, and returns a junk value when the minimum/maximum doesn't exist (e.g. the set is empty, not bounded, infinite, ...)

[Scott Morrison]

Perhaps we want function.max (which just takes a function into a type with has_le), and function.max_on (which takes such a function and a set in the domain type).

[Scott Morrison]

I guess the target type needs to have nonempty so we can pick a junk value.

[Scott Morrison]

For that matter we could provide a lawless has_Inf on any such type as well.

[Oliver Nash]

Returning to this, I think the following is what I really wanted:

import order.well_founded

noncomputable def function.argmin {α β : Type*} [nonempty α] [has_lt β] (f : α → β)
  (h : well_founded ((<) : β → β → Prop)) : α :=
well_founded.min (inv_image.wf f h) set.univ set.univ_nonempty

noncomputable def function.argmin_on {α β : Type*} [has_lt β] (f : α → β)
  (h : well_founded ((<) : β → β → Prop)) (s : set α) (hs : s.nonempty) : α :=
well_founded.min (inv_image.wf f h) s hs

This is just the specialisation of well_founded.min to the case that we have a function which takes values in a type carrying a well-founded <. It's still a very thin wrapper but I feel this might be worth adding.

Yes / no ?

[Heather Macbeth]

I believe I have also wanted this in the past!

[Oliver Nash]

I just searched Mathlib for uses of well_founded.min and by eye I'd say at least half are of this form with β = ℕ. I'll wait a while to see if there are dissenting opinions but if not I'll PR this + API later.

[Oliver Nash]

#8895 (dissenting opinions still welcome!)

[Scott Morrison]

I also have this in a branch I'm working on, so +1 from me!