can assume n is minimal

Stream: Is there code for X?

[Filippo A. E. Nuccio]

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]

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]

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]

I will certainly modify it, at any rate.

[Chris Hughes]

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]

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!