From b0c35d12fa3e9b7a8eb18f885a9377ab3c63e92f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 10 Jan 2021 14:47:09 +0000 Subject: [PATCH] chore(order/filter/basic): a few `simp` lemmas (#5685) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ### Changes in `order/filter/basic` * add `filter.inter_mem_sets_iff`; * rename `filter.Inter_mem_sets` to `filter.bInter_mem_sets`, make it an `iff` `[simp]` lemma; * add a version `filter.bInter_finset_mem_sets` with a protected alias `finset.Inter_mem_sets`; * rename `filter.sInter_mem_sets_of_finite` to `filter.sInter_mem_sets`, make it an `iff` `[simp]` lemma; * rename `filter.Inter_mem_sets_of_fintype` to `filter.Inter_mem_sets`, make it an `iff` `[simp]` lemma * add `eventually` versions of the `*Inter_mem_sets` lemmas. ### New `@[mono]` attributes * `set.union_subset_union` and `set.inter_subset_inter` instead of `monotone_union` and `monotone_inter`; `mono*` failed to make a progress with `s ∩ t ⊆ s' ∩ t'` goal. * `set.image2_subset` * `closure_mono` --- src/dynamics/omega_limit.lean | 18 +++------ src/order/filter/bases.lean | 8 ++-- src/order/filter/basic.lean | 56 ++++++++++++++++++-------- src/tactic/monotonicity/lemmas.lean | 3 +- src/topology/basic.lean | 10 +---- src/topology/constructions.lean | 2 +- src/topology/subset_properties.lean | 2 +- src/topology/uniform_space/basic.lean | 2 +- src/topology/uniform_space/cauchy.lean | 2 +- 9 files changed, 58 insertions(+), 45 deletions(-) diff --git a/src/dynamics/omega_limit.lean b/src/dynamics/omega_limit.lean index 40c58bd011960..db27d7394b65f 100644 --- a/src/dynamics/omega_limit.lean +++ b/src/dynamics/omega_limit.lean @@ -235,22 +235,16 @@ begin rw ←inter_Inter, exact subset.trans (inter_subset_right _ _) hn₂, end, - rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁, hg₂, hg₃⟩, + rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩, let w := (⋂ u ∈ g, u) ∩ v, - have hw₂ : w ∈ f, begin - apply inter_mem_sets _ hv₁, - rw ←sInter_eq_bInter, - exact sInter_mem_sets_of_finite hg₂ (λ _ hu, hg₁ hu), - end, + have hw₂ : w ∈ f, by simpa *, have hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ, from - calc _ ⊆ _ : hg₃ + calc k \ n ⊆ ⋃ u ∈ g, j u : hg₃ ... ⊆ (closure (image2 ϕ w s))ᶜ : begin - rw Union_subset_iff, intro u, - rw Union_subset_iff, intro hu, - rw compl_subset_compl, - apply closure_mono (image2_subset _ subset.rfl), - apply inter_subset_inter _ subset.rfl, + simp only [Union_subset_iff, compl_subset_compl], + intros u hu, + mono* using [w], exact Inter_subset_of_subset u (Inter_subset_of_subset hu subset.rfl), end, have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ, begin diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean index 7a5cdf9e9f6ed..ec89de1f6f70f 100644 --- a/src/order/filter/bases.lean +++ b/src/order/filter/bases.lean @@ -640,10 +640,10 @@ lemma antimono_seq_of_seq (s : ℕ → set α) : ∃ t : ℕ → set α, (∀ i j, i ≤ j → t j ⊆ t i) ∧ (⨅ i, 𝓟 $ s i) = ⨅ i, 𝓟 (t i) := begin use λ n, ⋂ m ≤ n, s m, split, - { intros i j hij a, simp, intros h i' hi'i, apply h, transitivity; assumption }, - apply le_antisymm; rw le_infi_iff; intro i, - { rw le_principal_iff, apply Inter_mem_sets (finite_le_nat _), - intros j hji, rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ }, + { exact λ i j hij, bInter_mono' (Iic_subset_Iic.2 hij) (λ n hn, subset.refl _) }, + apply le_antisymm; rw le_infi_iff; intro i, + { rw le_principal_iff, refine (bInter_mem_sets (finite_le_nat _)).2 (λ j hji, _), + rw ← le_principal_iff, apply infi_le_of_le j _, apply le_refl _ }, { apply infi_le_of_le i _, rw principal_mono, intro a, simp, intro h, apply h, refl }, end diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 1085e5728de75..0d6c6f11bf981 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -128,6 +128,10 @@ f.sets_of_superset lemma inter_mem_sets : ∀{s t}, s ∈ f → t ∈ f → s ∩ t ∈ f := f.inter_sets +@[simp] lemma inter_mem_sets_iff {s t} : s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f := +⟨λ h, ⟨mem_sets_of_superset h (inter_subset_left s t), + mem_sets_of_superset h (inter_subset_right s t)⟩, and_imp.2 inter_mem_sets⟩ + lemma univ_mem_sets' (h : ∀ a, a ∈ s) : s ∈ f := mem_sets_of_superset univ_mem_sets (assume x _, h x) @@ -138,22 +142,24 @@ lemma congr_sets (h : {x | x ∈ s ↔ x ∈ t} ∈ f) : s ∈ f ↔ t ∈ f := ⟨λ hs, mp_sets hs (mem_sets_of_superset h (λ x, iff.mp)), λ hs, mp_sets hs (mem_sets_of_superset h (λ x, iff.mpr))⟩ -lemma Inter_mem_sets {β : Type v} {s : β → set α} {is : set β} (hf : finite is) : - (∀i∈is, s i ∈ f) → (⋂i∈is, s i) ∈ f := -finite.induction_on hf - (assume hs, by simp only [univ_mem_sets, mem_empty_eq, Inter_neg, Inter_univ, not_false_iff]) - (assume i is _ hf hi hs, - have h₁ : s i ∈ f, from hs i (by simp), - have h₂ : (⋂x∈is, s x) ∈ f, from hi $ assume a ha, hs _ $ by simp only [ha, mem_insert_iff, or_true], - by simp [inter_mem_sets h₁ h₂]) +@[simp] lemma bInter_mem_sets {β : Type v} {s : β → set α} {is : set β} (hf : finite is) : + (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := +finite.induction_on hf (by simp) (λ i s hi _ hs, by simp [hs]) + +@[simp] lemma bInter_finset_mem_sets {β : Type v} {s : β → set α} (is : finset β) : + (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := +bInter_mem_sets is.finite_to_set -lemma sInter_mem_sets_of_finite {s : set (set α)} (hfin : finite s) (h_in : ∀ U ∈ s, U ∈ f) : - ⋂₀ s ∈ f := -by { rw sInter_eq_bInter, exact Inter_mem_sets hfin h_in } +alias bInter_finset_mem_sets ← finset.Inter_mem_sets +attribute [protected] finset.Inter_mem_sets -lemma Inter_mem_sets_of_fintype {β : Type v} {s : β → set α} [fintype β] (h : ∀i, s i ∈ f) : - (⋂i, s i) ∈ f := -by simpa using Inter_mem_sets finite_univ (λi hi, h i) +@[simp] lemma sInter_mem_sets {s : set (set α)} (hfin : finite s) : + ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f := +by rw [sInter_eq_bInter, bInter_mem_sets hfin] + +@[simp] lemma Inter_mem_sets {β : Type v} {s : β → set α} [fintype β] : + (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f := +by simpa using bInter_mem_sets finite_univ lemma exists_sets_subset_iff : (∃t ∈ f, t ⊆ s) ↔ s ∈ f := ⟨assume ⟨t, ht, ts⟩, mem_sets_of_superset ht ts, assume hs, ⟨s, hs, subset.refl _⟩⟩ @@ -459,7 +465,7 @@ begin let V := λ i, ⋂₀ σ i, have V_in : ∀ i, V i ∈ s i, { rintro ⟨i, i_in⟩, - apply sInter_mem_sets_of_finite (σfin _), + rw sInter_mem_sets (σfin _), apply σsub }, exact ⟨I, Ifin, V, V_in, tinter⟩ }, { rintro ⟨I, Ifin, V, V_in, h⟩, @@ -875,7 +881,7 @@ hp.mp (eventually_of_forall hq) @[simp] lemma eventually_and {p q : α → Prop} {f : filter α} : (∀ᶠ x in f, p x ∧ q x) ↔ (∀ᶠ x in f, p x) ∧ (∀ᶠ x in f, q x) := -⟨λ h, ⟨h.mono $ λ _, and.left, h.mono $ λ _, and.right⟩, λ h, h.1.and h.2⟩ +inter_mem_sets_iff lemma eventually.congr {f : filter α} {p q : α → Prop} (h' : ∀ᶠ x in f, p x) (h : ∀ᶠ x in f, p x ↔ q x) : ∀ᶠ x in f, q x := @@ -885,6 +891,24 @@ lemma eventually_congr {f : filter α} {p q : α → Prop} (h : ∀ᶠ x in f, p (∀ᶠ x in f, p x) ↔ (∀ᶠ x in f, q x) := ⟨λ hp, hp.congr h, λ hq, hq.congr $ by simpa only [iff.comm] using h⟩ +@[simp] lemma eventually_all {ι} [fintype ι] {l} {p : ι → α → Prop} : + (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x := +by simpa only [filter.eventually, set_of_forall] using Inter_mem_sets + +@[simp] lemma eventually_all_finite {ι} {I : set ι} (hI : I.finite) {l} {p : ι → α → Prop} : + (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ (∀ i ∈ I, ∀ᶠ x in l, p i x) := +by simpa only [filter.eventually, set_of_forall] using bInter_mem_sets hI + +alias eventually_all_finite ← set.finite.eventually_all +attribute [protected] set.finite.eventually_all + +@[simp] lemma eventually_all_finset {ι} (I : finset ι) {l} {p : ι → α → Prop} : + (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x := +I.finite_to_set.eventually_all + +alias eventually_all_finset ← finset.eventually_all +attribute [protected] finset.eventually_all + @[simp] lemma eventually_or_distrib_left {f : filter α} {p : Prop} {q : α → Prop} : (∀ᶠ x in f, p ∨ q x) ↔ (p ∨ ∀ᶠ x in f, q x) := classical.by_cases (λ h : p, by simp [h]) (λ h, by simp [h]) diff --git a/src/tactic/monotonicity/lemmas.lean b/src/tactic/monotonicity/lemmas.lean index af69a7e7573e4..12d1f686a47c2 100644 --- a/src/tactic/monotonicity/lemmas.lean +++ b/src/tactic/monotonicity/lemmas.lean @@ -68,9 +68,10 @@ end open set -attribute [mono] monotone_inter monotone_union +attribute [mono] inter_subset_inter union_subset_union sUnion_mono bUnion_mono sInter_subset_sInter bInter_mono image_subset preimage_mono prod_mono monotone_prod seq_mono + image2_subset attribute [mono] upper_bounds_mono_set lower_bounds_mono_set upper_bounds_mono_mem lower_bounds_mono_mem upper_bounds_mono lower_bounds_mono diff --git a/src/topology/basic.lean b/src/topology/basic.lean index 4773257065a2f..0966e88ac77e2 100644 --- a/src/topology/basic.lean +++ b/src/topology/basic.lean @@ -301,7 +301,7 @@ lemma is_closed.closure_subset_iff {s t : set α} (h₁ : is_closed t) : closure s ⊆ t ↔ s ⊆ t := ⟨subset.trans subset_closure, assume h, closure_minimal h h₁⟩ -lemma closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t := +@[mono] lemma closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t := closure_minimal (subset.trans h subset_closure) is_closed_closure lemma monotone_closure (α : Type*) [topological_space α] : monotone (@closure α _) := @@ -919,13 +919,7 @@ is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i), by simp only [mem_nhds_sets_iff]; exact assume i, ⟨(f i)ᶜ, subset.refl _, h₂ i, this i⟩, let ⟨t, h_sets, (h_fin : finite {i | (f i ∩ t).nonempty })⟩ := h₁ a in - calc 𝓝 a ≤ 𝓟 (t ∩ (⋂ i∈{i | (f i ∩ t).nonempty }, (f i)ᶜ)) : - begin - rw [le_principal_iff], - apply @filter.inter_mem_sets _ (𝓝 a) _ _ h_sets, - apply @filter.Inter_mem_sets _ (𝓝 a) _ _ _ h_fin, - exact assume i h, this i - end + calc 𝓝 a ≤ 𝓟 (t ∩ (⋂ i∈{i | (f i ∩ t).nonempty }, (f i)ᶜ)) : by simp * ... ≤ 𝓟 (⋃i, f i)ᶜ : begin simp only [principal_mono, subset_def, mem_compl_eq, mem_inter_eq, diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean index f35a95fd97962..f28a49dd791e1 100644 --- a/src/topology/constructions.lean +++ b/src/topology/constructions.lean @@ -627,7 +627,7 @@ by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, (hs _ ha).preimage (cont lemma set_pi_mem_nhds [Π a, topological_space (π a)] {i : set ι} {s : Π a, set (π a)} {x : Π a, π a} (hi : finite i) (hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)) : pi i s ∈ 𝓝 x := -by { rw [pi_def], exact Inter_mem_sets hi (λ a ha, (continuous_apply a).continuous_at (hs a ha)) } +by { rw [pi_def, bInter_mem_sets hi], exact λ a ha, (continuous_apply a).continuous_at (hs a ha) } lemma pi_eq_generate_from [∀a, topological_space (π a)] : Pi.topological_space = diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 8a533d6dd6bbf..f4ee3a5dcaa23 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -249,7 +249,7 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, cluster_pt let ⟨t, ht⟩ := h (λ i : f.sets, closure i.1) (λ i, is_closed_closure) (by simpa [eq_empty_iff_forall_not_mem, not_exists]) in have (⋂i∈t, subtype.val i) ∈ f, - from Inter_mem_sets t.finite_to_set $ assume i hi, i.2, + from t.Inter_mem_sets.2 $ assume i hi, i.2, have s ∩ (⋂i∈t, subtype.val i) ∈ f, from inter_mem_sets (le_principal_iff.1 hfs) this, have ∅ ∈ f, diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index f5a947ab536d4..1041c1f1a03c0 100644 --- a/src/topology/uniform_space/basic.lean +++ b/src/topology/uniform_space/basic.lean @@ -1392,7 +1392,7 @@ begin rcases comp_mem_uniformity_sets (is_open_uniformity.1 (hc₁ i) x h) with ⟨m', hm', mm'⟩, exact mem_bUnion hm' ⟨i, _, hm', λ y hy, mm' hy rfl⟩ }, rcases hs.elim_finite_subcover_image hu₁ hu₂ with ⟨b, bu, b_fin, b_cover⟩, - refine ⟨_, Inter_mem_sets b_fin bu, λ x hx, _⟩, + refine ⟨_, (bInter_mem_sets b_fin).2 bu, λ x hx, _⟩, rcases mem_bUnion_iff.1 (b_cover hx) with ⟨n, bn, i, m, hm, h⟩, refine ⟨i, λ y hy, h _⟩, exact prod_mk_mem_comp_rel (refl_mem_uniformity hm) (bInter_subset_of_mem bn hy) diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean index 4b8af361aba4d..7afd13b11511b 100644 --- a/src/topology/uniform_space/cauchy.lean +++ b/src/topology/uniform_space/cauchy.lean @@ -451,7 +451,7 @@ a sequence of monotonically decreasing sets `s n ∈ f` such that `(s n).prod (s def set_seq (n : ℕ) : set α := ⋂ m ∈ Iic n, (set_seq_aux hf U_mem m).val lemma set_seq_mem (n : ℕ) : set_seq hf U_mem n ∈ f := -Inter_mem_sets (finite_le_nat n) (λ m _, (set_seq_aux hf U_mem m).2.fst) +(bInter_mem_sets (finite_le_nat n)).2 (λ m _, (set_seq_aux hf U_mem m).2.fst) lemma set_seq_mono ⦃m n : ℕ⦄ (h : m ≤ n) : set_seq hf U_mem n ⊆ set_seq hf U_mem m := bInter_subset_bInter_left (λ k hk, le_trans hk h)