From ab316732ac69850d6d380bea5fa5ce3d72b3c13a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Iv=C3=A1n=20Sadofschi=20Costa?= Date: Thu, 9 Dec 2021 03:56:42 +0000 Subject: [PATCH] feat(data/finset/basic): val_le_iff_val_subset (#10603) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I'm not sure if we have something like this already on mathlib. The application of `val_le_of_val_subset` that I have in mind is to deduce ``` theorem polynomial.card_roots'' {F : Type u} [field F]{p : polynomial F}(h : p ≠ 0) {Z : finset F} (hZ : ∀ z ∈ Z, polynomial.eval z p = 0) : Z.card ≤ p.nat_degree ``` from [polynomial.card_roots' ](https://github.com/leanprover-community/mathlib/blob/1376f53dacd3c3ccd3c345b6b8552cce96c5d0c8/src/data/polynomial/ring_division.lean#L318) If this approach seems right, I will send the proof of `polynomial.card_roots''` in a follow up PR. Co-authored-by: Iván Sadofschi Costa --- src/data/finset/basic.lean | 3 +++ src/data/multiset/basic.lean | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index 50afcdcd0f287..f8c819dac9d4c 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -1782,6 +1782,9 @@ namespace finset @[simp] lemma val_to_finset [decidable_eq α] (s : finset α) : s.val.to_finset = s := by { ext, rw [multiset.mem_to_finset, ←mem_def] } +lemma val_le_iff_val_subset {a : finset α} {b : multiset α} : + a.val ≤ b ↔ a.val ⊆ b := multiset.le_iff_subset a.nodup + end finset namespace list diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean index 4b251bae7d416..f3f29f196de87 100644 --- a/src/data/multiset/basic.lean +++ b/src/data/multiset/basic.lean @@ -2032,6 +2032,9 @@ by induction n; simp [*, succ_nsmul', succ_mul, zero_nsmul] theorem count_pos {a : α} {s : multiset α} : 0 < count a s ↔ a ∈ s := by simp [count, countp_pos] +theorem one_le_count_iff_mem {a : α} {s : multiset α} : 1 ≤ count a s ↔ a ∈ s := +by rw [succ_le_iff, count_pos] + @[simp, priority 980] theorem count_eq_zero_of_not_mem {a : α} {s : multiset α} (h : a ∉ s) : count a s = 0 := by_contradiction $ λ h', h $ count_pos.1 (nat.pos_of_ne_zero h')