## Stream: Is there code for X?

### Topic: can assume n is minimal

#### Filippo A. E. Nuccio (Jan 16 2021 at 18:59):

I am proving a lemma where I construct a list of n elements (a multiset, actually) satisfying a certain property, and I want to assume that n is "minimal", in the sense that no subset of my multiset satisfies it. I ended up proving the following

lemma can_assume_min (p : multiset α → Prop) (s₀ : multiset α) (H : p s₀) :
∃ s ≤ s₀,  p s  ∧ (∀ a ∈ s, ¬ p (s.erase a)) :=


but since this is quite ubiquitous a strategy, I suspect that it must already be in mathlib, so I am double-checking before proposing a PR.

#### Damiano Testa (Jan 17 2021 at 09:39):

Could I suggest minimizing over all nonempty subsets? For instance, if your property is "having odd cardinality", I would probably expect a singleton, rather than a subset of odd cardinality.

#### Filippo A. E. Nuccio (Jan 17 2021 at 09:41):

Good point! I have actually created the PR #5783 and you can directly comment it there, so that it will appear to other reviewers.

#### Filippo A. E. Nuccio (Jan 17 2021 at 09:41):

I will certainly modify it, at any rate.

#### Chris Hughes (Jan 18 2021 at 07:41):

I think you can use well_founded.min with a proof that the subset relation on multisets is well founded. To prove well foundedness, you can use the fact that it implies the size decreases, so measure_wf is what you need.

#### Filippo A. E. Nuccio (Jan 18 2021 at 15:36):

Thanks! I also came up with the idea that existence of min could be useful, but I had no idea on how to implement this. I will give it a try!

Last updated: May 07 2021 at 23:11 UTC