# Zulip Chat Archive

## 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