From 1cd228629592ddb002dc85b3efa74f550abedf59 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 27 Jan 2021 08:41:48 +0000 Subject: [PATCH] chore(data/finset/preimage): add missing simp lemmas (#5902) --- src/data/finset/preimage.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/data/finset/preimage.lean b/src/data/finset/preimage.lean index d8f7c34a28b10..972bbff13b4ce 100644 --- a/src/data/finset/preimage.lean +++ b/src/data/finset/preimage.lean @@ -34,6 +34,30 @@ set.finite.mem_to_finset (hf : set.inj_on f (f ⁻¹' ↑s)) : (↑(preimage s f hf) : set α) = f ⁻¹' ↑s := set.finite.coe_to_finset _ +@[simp] lemma preimage_empty {f : α → β} : preimage ∅ f (by simp [inj_on]) = ∅ := +finset.coe_injective (by simp) + +@[simp] lemma preimage_univ {f : α → β} [fintype α] [fintype β] (hf) : + preimage univ f hf = univ := +finset.coe_injective (by simp) + +@[simp] lemma preimage_inter [decidable_eq α] [decidable_eq β] {f : α → β} {s t : finset β} + (hs : set.inj_on f (f ⁻¹' ↑s)) (ht : set.inj_on f (f ⁻¹' ↑t)) : + preimage (s ∩ t) f (λ x₁ hx₁ x₂ hx₂, hs (mem_of_mem_inter_left hx₁) (mem_of_mem_inter_left hx₂)) + = preimage s f hs ∩ preimage t f ht := +finset.coe_injective (by simp) + +@[simp] lemma preimage_union [decidable_eq α] [decidable_eq β] {f : α → β} {s t : finset β} (hst) : + preimage (s ∪ t) f hst + = preimage s f (λ x₁ hx₁ x₂ hx₂, hst (mem_union_left _ hx₁) (mem_union_left _ hx₂)) + ∪ preimage t f (λ x₁ hx₁ x₂ hx₂, hst (mem_union_right _ hx₁) (mem_union_right _ hx₂)) := +finset.coe_injective (by simp) + +@[simp] lemma preimage_compl [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] + {f : α → β} (s : finset β) (hf : function.injective f) : + preimage sᶜ f (hf.inj_on _) = (preimage s f (hf.inj_on _))ᶜ := +finset.coe_injective (by simp) + lemma monotone_preimage {f : α → β} (h : injective f) : monotone (λ s, preimage s f (h.inj_on _)) := λ s t hst x hx, mem_preimage.2 (hst $ mem_preimage.1 hx)