diff --git a/roadmap/topology/shrinking_lemma.lean b/roadmap/topology/shrinking_lemma.lean index 9996716905781..5b7f6e108871d 100644 --- a/roadmap/topology/shrinking_lemma.lean +++ b/roadmap/topology/shrinking_lemma.lean @@ -34,7 +34,7 @@ cover so that the closure of each new open set is contained in the corresponding set. -/ lemma roadmap.shrinking_lemma {X : Type u} [topological_space X] [normal_space X] {s : set X} (hs : is_closed s) {α : Type v} (u : α → set X) (uo : ∀ a, is_open (u a)) - (uf : ∀ x, finite {a | x ∈ u a}) (su : s ⊆ Union u) : + (uf : ∀ x, {a | x ∈ u a}.finite) (su : s ⊆ Union u) : ∃ v : α → set X, s ⊆ Union v ∧ ∀ a, is_open (v a) ∧ closure (v a) ⊆ u a := todo /- diff --git a/src/algebra/big_operators/finprod.lean b/src/algebra/big_operators/finprod.lean index 57b78953ecc23..e96a2dda72ff2 100644 --- a/src/algebra/big_operators/finprod.lean +++ b/src/algebra/big_operators/finprod.lean @@ -87,13 +87,13 @@ open_locale classical /-- Sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Zero otherwise. -/ @[irreducible] noncomputable def finsum {M α} [add_comm_monoid M] (f : α → M) : M := -if h : finite (support (f ∘ plift.down)) then ∑ i in h.to_finset, f i.down else 0 +if h : (support (f ∘ plift.down)).finite then ∑ i in h.to_finset, f i.down else 0 /-- Product of `f x` as `x` ranges over the elements of the multiplicative support of `f`, if it's finite. One otherwise. -/ @[irreducible, to_additive] noncomputable def finprod (f : α → M) : M := -if h : finite (mul_support (f ∘ plift.down)) then ∏ i in h.to_finset, f i.down else 1 +if h : (mul_support (f ∘ plift.down)).finite then ∏ i in h.to_finset, f i.down else 1 end @@ -102,7 +102,7 @@ localized "notation `∑ᶠ` binders `, ` r:(scoped:67 f, finsum f) := r" in big localized "notation `∏ᶠ` binders `, ` r:(scoped:67 f, finprod f) := r" in big_operators @[to_additive] lemma finprod_eq_prod_plift_of_mul_support_to_finset_subset - {f : α → M} (hf : finite (mul_support (f ∘ plift.down))) {s : finset (plift α)} + {f : α → M} (hf : (mul_support (f ∘ plift.down)).finite) {s : finset (plift α)} (hs : hf.to_finset ⊆ s) : ∏ᶠ i, f i = ∏ i in s, f i.down := begin @@ -191,7 +191,7 @@ lemma one_le_finprod' {M : Type*} [ordered_comm_monoid M] {f : α → M} (hf : finprod_induction _ le_rfl (λ _ _, one_le_mul) hf @[to_additive] lemma monoid_hom.map_finprod_plift (f : M →* N) (g : α → M) - (h : finite (mul_support $ g ∘ plift.down)) : + (h : (mul_support $ g ∘ plift.down).finite) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) := begin rw [finprod_eq_prod_plift_of_mul_support_subset h.coe_to_finset.ge, @@ -277,7 +277,7 @@ begin end @[to_additive] lemma finprod_eq_prod_of_mul_support_to_finset_subset (f : α → M) - (hf : finite (mul_support f)) {s : finset α} (h : hf.to_finset ⊆ s) : + (hf : (mul_support f).finite) {s : finset α} (h : hf.to_finset ⊆ s) : ∏ᶠ i, f i = ∏ i in s, f i := finprod_eq_prod_of_mul_support_subset _ $ λ x hx, h $ hf.mem_to_finset.2 hx @@ -326,7 +326,7 @@ begin end @[to_additive] lemma finprod_cond_ne (f : α → M) (a : α) [decidable_eq α] - (hf : finite (mul_support f)) : (∏ᶠ i ≠ a, f i) = ∏ i in hf.to_finset.erase a, f i := + (hf : (mul_support f).finite) : (∏ᶠ i ≠ a, f i) = ∏ i in hf.to_finset.erase a, f i := begin apply finprod_cond_eq_prod_of_cond_iff, intros x hx, @@ -670,7 +670,7 @@ lemma finprod_mem_image' {s : set β} {g : β → α} (hg : (s ∩ mul_support ( ∏ᶠ i ∈ g '' s, f i = ∏ᶠ j ∈ s, f (g j) := begin classical, - by_cases hs : finite (s ∩ mul_support (f ∘ g)), + by_cases hs : (s ∩ mul_support (f ∘ g)).finite, { have hg : ∀ (x ∈ hs.to_finset) (y ∈ hs.to_finset), g x = g y → x = y, by simpa only [hs.mem_to_finset], rw [finprod_mem_eq_prod _ hs, ← finset.prod_image hg], @@ -814,7 +814,7 @@ lemma finprod_mem_sUnion {t : set (set α)} (h : t.pairwise_disjoint id) (ht₀ ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a := by { rw set.sUnion_eq_bUnion, exact finprod_mem_bUnion h ht₀ ht₁ } -@[to_additive] lemma mul_finprod_cond_ne (a : α) (hf : finite (mul_support f)) : +@[to_additive] lemma mul_finprod_cond_ne (a : α) (hf : (mul_support f).finite) : f a * (∏ᶠ i ≠ a, f i) = ∏ᶠ i, f i := begin classical, @@ -858,7 +858,7 @@ finprod_nonneg $ λ x, finprod_nonneg $ hf x @[to_additive] lemma single_le_finprod {M : Type*} [ordered_comm_monoid M] (i : α) {f : α → M} - (hf : finite (mul_support f)) (h : ∀ j, 1 ≤ f j) : + (hf : (mul_support f).finite) (h : ∀ j, 1 ≤ f j) : f i ≤ ∏ᶠ j, f j := by classical; calc f i ≤ ∏ j in insert i hf.to_finset, f j : @@ -867,7 +867,7 @@ calc f i ≤ ∏ j in insert i hf.to_finset, f j : (finprod_eq_prod_of_mul_support_to_finset_subset _ hf (finset.subset_insert _ _)).symm lemma finprod_eq_zero {M₀ : Type*} [comm_monoid_with_zero M₀] (f : α → M₀) (x : α) - (hx : f x = 0) (hf : finite (mul_support f)) : + (hx : f x = 0) (hf : (mul_support f).finite) : ∏ᶠ x, f x = 0 := begin nontriviality, diff --git a/src/algebra/star/pointwise.lean b/src/algebra/star/pointwise.lean index ad20032b19e13..15a65ea50044a 100644 --- a/src/algebra/star/pointwise.lean +++ b/src/algebra/star/pointwise.lean @@ -91,7 +91,7 @@ equiv.star.surjective.preimage_subset_preimage_iff lemma star_subset [has_involutive_star α] {s t : set α} : s⋆ ⊆ t ↔ s ⊆ t⋆ := by { rw [← star_subset_star, star_star] } -lemma finite.star [has_involutive_star α] {s : set α} (hs : finite s) : finite s⋆ := +lemma finite.star [has_involutive_star α] {s : set α} (hs : s.finite) : s⋆.finite := hs.preimage $ star_injective.inj_on _ lemma star_singleton {β : Type*} [has_involutive_star β] (x : β) : ({x} : set β)⋆ = {x⋆} := diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 0620f41de331e..9d77210e94389 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -302,7 +302,7 @@ begin (hw₁.symm ▸ zero_lt_one) (λ x hx, hx) } end -lemma set.finite.convex_hull_eq {s : set E} (hs : finite s) : +lemma set.finite.convex_hull_eq {s : set E} (hs : s.finite) : convex_hull R s = {x : E | ∃ (w : E → R) (hw₀ : ∀ y ∈ s, 0 ≤ w y) (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x} := by simpa only [set.finite.coe_to_finset, set.finite.mem_to_finset, exists_prop] @@ -402,7 +402,7 @@ under the linear map sending each function `w` to `∑ x in s, w x • x`. Since we have no sums over finite sets, we use sum over `@finset.univ _ hs.fintype`. The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so that later we will not need to prove that this map is linear. -/ -lemma set.finite.convex_hull_eq_image {s : set E} (hs : finite s) : +lemma set.finite.convex_hull_eq_image {s : set E} (hs : s.finite) : convex_hull R s = by haveI := hs.fintype; exact (⇑(∑ x : s, (@linear_map.proj R s _ (λ i, R) _ _ x).smul_right x.1)) '' (std_simplex R s) := begin diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean index ab37411b7b782..28f625b7a4016 100644 --- a/src/analysis/convex/topology.lean +++ b/src/analysis/convex/topology.lean @@ -213,7 +213,7 @@ variables [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] /-- Convex hull of a finite set is compact. -/ -lemma set.finite.compact_convex_hull {s : set E} (hs : finite s) : +lemma set.finite.compact_convex_hull {s : set E} (hs : s.finite) : is_compact (convex_hull ℝ s) := begin rw [hs.convex_hull_eq_image], @@ -223,7 +223,7 @@ begin end /-- Convex hull of a finite set is closed. -/ -lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : finite s) : +lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : s.finite) : is_closed (convex_hull ℝ s) := hs.compact_convex_hull.is_closed diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean index c030ac50a187f..1d84304c214fd 100644 --- a/src/data/polynomial/ring_division.lean +++ b/src/data/polynomial/ring_division.lean @@ -622,7 +622,7 @@ finset_coe.fintype _ lemma root_set_finite (p : T[X]) (S : Type*) [comm_ring S] [is_domain S] [algebra T S] : (p.root_set S).finite := -⟨polynomial.root_set_fintype p S⟩ +set.finite_of_fintype _ theorem mem_root_set_iff' {p : T[X]} {S : Type*} [comm_ring S] [is_domain S] [algebra T S] (hp : p.map (algebra_map T S) ≠ 0) (a : S) : diff --git a/src/data/set/countable.lean b/src/data/set/countable.lean index 593b5da0df82f..3a4709cfd2e0e 100644 --- a/src/data/set/countable.lean +++ b/src/data/set/countable.lean @@ -184,7 +184,7 @@ by simp only [insert_eq, countable_union, countable_singleton, true_and] lemma countable.insert {s : set α} (a : α) (h : countable s) : countable (insert a s) := countable_insert.2 h -lemma finite.countable {s : set α} : finite s → countable s +lemma finite.countable {s : set α} : s.finite → countable s | ⟨h⟩ := trunc.nonempty (by exactI fintype.trunc_encodable s) lemma subsingleton.countable {s : set α} (hs : s.subsingleton) : countable s := @@ -198,7 +198,7 @@ lemma countable_is_bot (α : Type*) [partial_order α] : countable {x : α | is_ /-- The set of finite subsets of a countable set is countable. -/ lemma countable_set_of_finite_subset {s : set α} : countable s → - countable {t | finite t ∧ t ⊆ s} | ⟨h⟩ := + countable {t | set.finite t ∧ t ⊆ s} | ⟨h⟩ := begin resetI, refine countable.mono _ (countable_range diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean index 103ede850540a..7c8b9ee68e17b 100644 --- a/src/data/set/finite.lean +++ b/src/data/set/finite.lean @@ -49,10 +49,18 @@ namespace set /-- A set is finite if there is a `finset` with the same elements. This is represented as there being a `fintype` instance for the set -coerced to a type. -/ -inductive finite (s : set α) : Prop +coerced to a type. + +Note: this is a custom inductive type rather than `nonempty (fintype s)` +so that it won't be frozen as a local instance. -/ +@[protected] inductive finite (s : set α) : Prop | intro : fintype s → finite +-- The `protected` attribute does not take effect within the same namespace block. +end set + +namespace set + /-- Constructor for `set.finite` with the `fintype` as an instance argument. -/ theorem finite_of_fintype (s : set α) [h : fintype s] : s.finite := ⟨h⟩ @@ -81,12 +89,12 @@ by { casesI h, exact ⟨s.to_finset, s.coe_to_finset⟩ } /-- Finite sets can be lifted to finsets. -/ instance : can_lift (set α) (finset α) := { coe := coe, - cond := finite, + cond := set.finite, prf := λ s hs, hs.exists_finset_coe } /-- A set is infinite if it is not finite. -Protected so that it does not conflict with global `infinite`. -/ +This is protected so that it does not conflict with global `infinite`. -/ protected def infinite (s : set α) : Prop := ¬ s.finite @[simp] lemma not_infinite {s : set α} : ¬ s.infinite ↔ s.finite := not_not @@ -334,7 +342,7 @@ theorem finite_univ [fintype α] : (@univ α).finite := finite_of_fintype _ theorem finite.union {s t : set α} (hs : s.finite) (ht : t.finite) : (s ∪ t).finite := by { classical, casesI hs, casesI ht, apply finite_of_fintype } -lemma finite.sup {s t : set α} : finite s → finite t → finite (s ⊔ t) := finite.union +lemma finite.sup {s t : set α} : s.finite → t.finite → (s ⊔ t).finite := finite.union theorem finite.sep {s : set α} (hs : s.finite) (p : α → Prop) : {a ∈ s | p a}.finite := by { classical, casesI hs, apply finite_of_fintype } @@ -345,10 +353,10 @@ by { classical, casesI hs, apply finite_of_fintype } theorem finite.inter_of_right {s : set α} (hs : s.finite) (t : set α) : (t ∩ s).finite := by { classical, casesI hs, apply finite_of_fintype } -theorem finite.inf_of_left {s : set α} (h : finite s) (t : set α) : finite (s ⊓ t) := +theorem finite.inf_of_left {s : set α} (h : s.finite) (t : set α) : (s ⊓ t).finite := h.inter_of_left t -theorem finite.inf_of_right {s : set α} (h : finite s) (t : set α) : finite (t ⊓ s) := +theorem finite.inf_of_right {s : set α} (h : s.finite) (t : set α) : (t ⊓ s).finite := h.inter_of_right t theorem finite.subset {s : set α} (hs : s.finite) {t : set α} (ht : t ⊆ s) : t.finite := @@ -357,14 +365,15 @@ by { classical, casesI hs, haveI := set.fintype_subset _ ht, apply finite_of_fin theorem finite.diff {s : set α} (hs : s.finite) (t : set α) : (s \ t).finite := by { classical, casesI hs, apply finite_of_fintype } -theorem finite.of_diff {s t : set α} (hd : finite (s \ t)) (ht : finite t) : finite s := +theorem finite.of_diff {s t : set α} (hd : (s \ t).finite) (ht : t.finite) : s.finite := (hd.union ht).subset $ subset_diff_union _ _ theorem finite_Union [fintype (plift ι)] {f : ι → set α} (H : ∀ i, (f i).finite) : (⋃ i, f i).finite := by { classical, haveI := λ i, (H i).fintype, apply finite_of_fintype } -theorem finite.sUnion {s : set (set α)} (hs : s.finite) (H : ∀ t ∈ s, finite t) : (⋃₀ s).finite := +theorem finite.sUnion {s : set (set α)} (hs : s.finite) (H : ∀ t ∈ s, set.finite t) : + (⋃₀ s).finite := by { classical, casesI hs, haveI := λ (i : s), (H i i.2).fintype, apply finite_of_fintype } theorem finite.bUnion {ι} {s : set ι} (hs : s.finite) @@ -382,7 +391,7 @@ theorem finite.sInter {α : Type*} {s : set (set α)} {t : set α} (ht : t ∈ s hf.subset (sInter_subset_of_mem ht) theorem finite.bind {α β} {s : set α} {f : α → set β} (h : s.finite) (hf : ∀ a ∈ s, (f a).finite) : - finite (s >>= f) := + (s >>= f).finite := h.bUnion hf @[simp] theorem finite_empty : (∅ : set α).finite := finite_of_fintype _ @@ -401,51 +410,51 @@ theorem finite_range (f : ι → α) [fintype (plift ι)] : (range f).finite := by { classical, apply finite_of_fintype } lemma finite.dependent_image {s : set α} (hs : s.finite) (F : Π i ∈ s, β) : - finite {y : β | ∃ x (hx : x ∈ s), y = F x hx} := + {y : β | ∃ x (hx : x ∈ s), y = F x hx}.finite := by { casesI hs, simpa [range, eq_comm] using finite_range (λ x : s, F x x.2) } -theorem finite.map {α β} {s : set α} : ∀ (f : α → β), finite s → finite (f <$> s) := +theorem finite.map {α β} {s : set α} : ∀ (f : α → β), s.finite → (f <$> s).finite := finite.image theorem finite.of_finite_image {s : set α} {f : α → β} (h : (f '' s).finite) (hi : set.inj_on f s) : - finite s := + s.finite := by { casesI h, exact ⟨fintype.of_injective (λ a, (⟨f a.1, mem_image_of_mem f a.2⟩ : f '' s)) (λ a b eq, subtype.eq $ hi a.2 b.2 $ subtype.ext_iff_val.1 eq)⟩ } theorem finite.of_preimage {f : α → β} {s : set β} (h : (f ⁻¹' s).finite) (hf : surjective f) : - finite s := + s.finite := hf.image_preimage s ▸ h.image _ theorem finite.preimage {s : set β} {f : α → β} - (I : set.inj_on f (f⁻¹' s)) (h : finite s) : finite (f ⁻¹' s) := + (I : set.inj_on f (f⁻¹' s)) (h : s.finite) : (f ⁻¹' s).finite := (h.subset (image_preimage_subset f s)).of_finite_image I theorem finite.preimage_embedding {s : set β} (f : α ↪ β) (h : s.finite) : (f ⁻¹' s).finite := h.preimage (λ _ _ _ _ h', f.injective h') -lemma finite_lt_nat (n : ℕ) : finite {i | i < n} := finite_of_fintype _ +lemma finite_lt_nat (n : ℕ) : set.finite {i | i < n} := finite_of_fintype _ -lemma finite_le_nat (n : ℕ) : finite {i | i ≤ n} := finite_of_fintype _ +lemma finite_le_nat (n : ℕ) : set.finite {i | i ≤ n} := finite_of_fintype _ lemma finite.prod {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) : (s ×ˢ t : set (α × β)).finite := by { classical, casesI hs, casesI ht, apply finite_of_fintype } lemma finite.image2 (f : α → β → γ) {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) : - finite (image2 f s t) := + (image2 f s t).finite := by { classical, casesI hs, casesI ht, apply finite_of_fintype } theorem finite.seq {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) : - finite (f.seq s) := + (f.seq s).finite := by { classical, casesI hf, casesI hs, apply finite_of_fintype } theorem finite.seq' {α β : Type u} {f : set (α → β)} {s : set α} (hf : f.finite) (hs : s.finite) : - finite (f <*> s) := + (f <*> s).finite := hf.seq hs -theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} := finite_of_fintype _ +theorem finite_mem_finset (s : finset α) : {a | a ∈ s}.finite := finite_of_fintype _ -lemma subsingleton.finite {s : set α} (h : s.subsingleton) : finite s := +lemma subsingleton.finite {s : set α} (h : s.subsingleton) : s.finite := h.induction_on finite_empty finite_singleton theorem exists_finite_iff_finset {p : set α → Prop} : @@ -454,7 +463,7 @@ theorem exists_finite_iff_finset {p : set α → Prop} : λ ⟨s, hs⟩, ⟨↑s, finite_mem_finset s, hs⟩⟩ /-- There are finitely many subsets of a given finite set -/ -lemma finite.finite_subsets {α : Type u} {a : set α} (h : finite a) : finite {b | b ⊆ a} := +lemma finite.finite_subsets {α : Type u} {a : set α} (h : a.finite) : {b | b ⊆ a}.finite := ⟨fintype.of_finset ((finset.powerset h.to_finset).map finset.coe_emb.1) $ λ s, by simpa [← @exists_finite_iff_finset α (λ t, t ⊆ a ∧ t = s), subset_to_finset_iff, ← and.assoc] using h.subset⟩ @@ -475,11 +484,11 @@ lemma union_finset_finite_of_range_finite (f : α → finset β) (h : (range f). (⋃ a, (f a : set β)).finite := by { rw ← bUnion_range, exact h.bUnion (λ y hy, finite_of_fintype y) } -lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f)) - (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) := +lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : (range f).finite) + (hg : (range g).finite) : (range (λ x, if p x then f x else g x)).finite := (hf.union hg).subset range_ite_subset -lemma finite_range_const {c : β} : finite (range (λ x : α, c)) := +lemma finite_range_const {c : β} : (range (λ x : α, c)).finite := (finite_singleton c).subset range_const_subset end set_finite_constructors @@ -505,14 +514,14 @@ lemma finite.to_finset_insert [decidable_eq α] {a : α} {s : set α} (hs : s.fi (hs.insert a).to_finset = insert a hs.to_finset := finset.ext $ by simp -lemma finite.fin_embedding {s : set α} (h : finite s) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s := +lemma finite.fin_embedding {s : set α} (h : s.finite) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s := ⟨_, (fintype.equiv_fin (h.to_finset : set α)).symm.as_embedding, by simp⟩ lemma finite.fin_param {s : set α} (h : s.finite) : ∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s := let ⟨n, f, hf⟩ := h.fin_embedding in ⟨n, f, f.injective, hf⟩ -lemma finite_option {s : set (option α)} : s.finite ↔ finite {x : α | some x ∈ s} := +lemma finite_option {s : set (option α)} : s.finite ↔ {x : α | some x ∈ s}.finite := ⟨λ h, h.preimage_embedding embedding.some, λ h, ((h.image some).insert none).subset $ λ x, option.cases_on x (λ _, or.inl rfl) (λ x hx, or.inr $ mem_image_of_mem _ hx)⟩ @@ -526,7 +535,7 @@ lemma forall_finite_image_eval_iff {δ : Type*} [fintype δ] {κ : δ → Type*} (∀ d, (eval d '' s).finite) ↔ s.finite := ⟨λ h, (finite.pi h).subset $ subset_pi_eval_image _ _, λ h d, h.image _⟩ -lemma finite_subset_Union {s : set α} (hs : finite s) +lemma finite_subset_Union {s : set α} (hs : s.finite) {ι} {t : ι → set α} (h : s ⊆ ⋃ i, t i) : ∃ I : set ι, I.finite ∧ s ⊆ ⋃ i ∈ I, t i := begin casesI hs, @@ -557,7 +566,7 @@ let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in @[elab_as_eliminator] theorem finite.induction_on {C : set α → Prop} {s : set α} (h : s.finite) - (H0 : C ∅) (H1 : ∀ {a s}, a ∉ s → finite s → C s → C (insert a s)) : C s := + (H0 : C ∅) (H1 : ∀ {a s}, a ∉ s → set.finite s → C s → C (insert a s)) : C s := let ⟨t⟩ := h in by exactI match s.to_finset, @mem_to_finset _ s _ with | ⟨l, nd⟩, al := begin @@ -576,9 +585,9 @@ end @[elab_as_eliminator] theorem finite.dinduction_on {C : ∀ (s : set α), s.finite → Prop} {s : set α} (h : s.finite) (H0 : C ∅ finite_empty) - (H1 : ∀ {a s}, a ∉ s → ∀ h : finite s, C s h → C (insert a s) (h.insert a)) : + (H1 : ∀ {a s}, a ∉ s → ∀ h : set.finite s, C s h → C (insert a s) (h.insert a)) : C s h := -have ∀ h : finite s, C s h, +have ∀ h : s.finite, C s h, from finite.induction_on h (λ h, H0) (λ a s has hs ih h, H1 has hs (ih _)), this h @@ -764,10 +773,10 @@ in ⟨a, has, λ h, haf $ finset.mem_coe.1 h⟩ /-! ### Order properties -/ -lemma finite_is_top (α : Type*) [partial_order α] : finite {x : α | is_top x} := +lemma finite_is_top (α : Type*) [partial_order α] : {x : α | is_top x}.finite := (subsingleton_is_top α).finite -lemma finite_is_bot (α : Type*) [partial_order α] : finite {x : α | is_bot x} := +lemma finite_is_bot (α : Type*) [partial_order α] : {x : α | is_bot x}.finite := (subsingleton_is_bot α).finite theorem infinite.exists_lt_map_eq_of_maps_to [linear_order α] {s : set α} {t : set β} {f : α → β} @@ -785,12 +794,12 @@ begin exact ⟨a, b, h⟩, end -lemma exists_min_image [linear_order β] (s : set α) (f : α → β) (h1 : finite s) : +lemma exists_min_image [linear_order β] (s : set α) (f : α → β) (h1 : s.finite) : s.nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b | ⟨x, hx⟩ := by simpa only [exists_prop, finite.mem_to_finset] using h1.to_finset.exists_min_image f ⟨x, h1.mem_to_finset.2 hx⟩ -lemma exists_max_image [linear_order β] (s : set α) (f : α → β) (h1 : finite s) : +lemma exists_max_image [linear_order β] (s : set α) (f : α → β) (h1 : s.finite) : s.nonempty → ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a | ⟨x, hx⟩ := by simpa only [exists_prop, finite.mem_to_finset] using h1.to_finset.exists_max_image f ⟨x, h1.mem_to_finset.2 hx⟩ @@ -888,7 +897,7 @@ lemma Inter_Union_of_antitone {ι ι' α : Type*} [fintype ι] [preorder ι'] [i infi_supr_of_antitone hs lemma Union_pi_of_monotone {ι ι' : Type*} [linear_order ι'] [nonempty ι'] {α : ι → Type*} - {I : set ι} {s : Π i, ι' → set (α i)} (hI : finite I) (hs : ∀ i ∈ I, monotone (s i)) : + {I : set ι} {s : Π i, ι' → set (α i)} (hI : I.finite) (hs : ∀ i ∈ I, monotone (s i)) : (⋃ j : ι', I.pi (λ i, s i j)) = I.pi (λ i, ⋃ j, s i j) := begin simp only [pi_def, bInter_eq_Inter, preimage_Union], @@ -906,7 +915,7 @@ lemma range_find_greatest_subset {P : α → ℕ → Prop} [∀ x, decidable_pre by { rw range_subset_iff, intro x, simp [nat.lt_succ_iff, nat.find_greatest_le] } lemma finite_range_find_greatest {P : α → ℕ → Prop} [∀ x, decidable_pred (P x)] {b : ℕ} : - finite (range (λ x, nat.find_greatest (P x) b)) := + (range (λ x, nat.find_greatest (P x) b)).finite := (finite_of_fintype ↑(finset.range (b + 1))).subset range_find_greatest_subset lemma finite.exists_maximal_wrt [partial_order β] (f : α → β) (s : set α) (h : set.finite s) : @@ -935,11 +944,11 @@ section variables [semilattice_sup α] [nonempty α] {s : set α} /--A finite set is bounded above.-/ -protected lemma finite.bdd_above (hs : finite s) : bdd_above s := +protected lemma finite.bdd_above (hs : s.finite) : bdd_above s := finite.induction_on hs bdd_above_empty $ λ a s _ _ h, h.insert a /--A finite union of sets which are all bounded above is still bounded above.-/ -lemma finite.bdd_above_bUnion {I : set β} {S : β → set α} (H : finite I) : +lemma finite.bdd_above_bUnion {I : set β} {S : β → set α} (H : I.finite) : (bdd_above (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_above (S i)) := finite.induction_on H (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff]) @@ -959,10 +968,10 @@ section variables [semilattice_inf α] [nonempty α] {s : set α} /--A finite set is bounded below.-/ -protected lemma finite.bdd_below (hs : finite s) : bdd_below s := @finite.bdd_above αᵒᵈ _ _ _ hs +protected lemma finite.bdd_below (hs : s.finite) : bdd_below s := @finite.bdd_above αᵒᵈ _ _ _ hs /--A finite union of sets which are all bounded below is still bounded below.-/ -lemma finite.bdd_below_bUnion {I : set β} {S : β → set α} (H : finite I) : +lemma finite.bdd_below_bUnion {I : set β} {S : β → set α} (H : I.finite) : bdd_below (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, bdd_below (S i) := @finite.bdd_above_bUnion αᵒᵈ _ _ _ _ _ H diff --git a/src/data/set/pointwise.lean b/src/data/set/pointwise.lean index 47f631c225661..92665764ae987 100644 --- a/src/data/set/pointwise.lean +++ b/src/data/set/pointwise.lean @@ -137,7 +137,7 @@ inv_involutive.surjective.nonempty_preimage @[to_additive] lemma nonempty.inv (h : s.nonempty) : s⁻¹.nonempty := nonempty_inv.2 h -@[to_additive] lemma finite.inv (hs : finite s) : finite s⁻¹ := +@[to_additive] lemma finite.inv (hs : s.finite) : s⁻¹.finite := hs.preimage $ inv_injective.inj_on _ @[simp, to_additive] @@ -257,7 +257,7 @@ lemma mul_Inter₂_subset (s : set α) (t : Π i, κ i → set α) : s * (⋂ i j, t i j) ⊆ ⋂ i j, s * t i j := image2_Inter₂_subset_right _ _ _ -@[to_additive] lemma finite.mul : finite s → finite t → finite (s * t) := finite.image2 _ +@[to_additive] lemma finite.mul : s.finite → t.finite → (s * t).finite := finite.image2 _ /-- Multiplication preserves finiteness. -/ @[to_additive "Addition preserves finiteness."] @@ -861,7 +861,7 @@ lemma smul_Inter₂_subset (s : set α) (t : Π i, κ i → set β) : s • (⋂ i j, t i j) ⊆ ⋂ i j, s • t i j := image2_Inter₂_subset_right _ _ _ -@[to_additive] lemma finite.smul : finite s → finite t → finite (s • t) := finite.image2 _ +@[to_additive] lemma finite.smul : s.finite → t.finite → (s • t).finite := finite.image2 _ end has_scalar @@ -904,7 +904,7 @@ lemma smul_set_Inter₂_subset (a : α) (t : Π i, κ i → set β) : image_Inter₂_subset _ _ @[to_additive] lemma nonempty.smul_set : s.nonempty → (a • s).nonempty := nonempty.image _ -@[to_additive] lemma finite.smul_set : finite s → finite (a • s) := finite.image _ +@[to_additive] lemma finite.smul_set : s.finite → (a • s).finite := finite.image _ end has_scalar_set @@ -1074,7 +1074,7 @@ lemma vsub_Inter₂_subset (s : set β) (t : Π i, κ i → set β) : s -ᵥ (⋂ i j, t i j) ⊆ ⋂ i j, s -ᵥ t i j := image2_Inter₂_subset_right _ _ _ -lemma finite.vsub (hs : finite s) (ht : finite t) : finite (s -ᵥ t) := hs.image2 _ ht +lemma finite.vsub (hs : s.finite) (ht : t.finite) : set.finite (s -ᵥ t) := hs.image2 _ ht end vsub diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean index aa8c27228f419..eeb3b8f5a8f2c 100644 --- a/src/linear_algebra/finite_dimensional.lean +++ b/src/linear_algebra/finite_dimensional.lean @@ -1295,10 +1295,10 @@ protected noncomputable def set.finrank (s : set V) : ℕ := finrank K (span K s variable {K} -lemma finrank_span_le_card (s : set V) [fin : fintype s] : +lemma finrank_span_le_card (s : set V) [fintype s] : finrank K (span K s) ≤ s.to_finset.card := begin - haveI := span_of_finite K ⟨fin⟩, + haveI := span_of_finite K (set.finite_of_fintype s), have : module.rank K (span K s) ≤ #s := dim_span_le s, rw [←finrank_eq_dim, cardinal.mk_fintype, ←set.to_finset_card] at this, exact_mod_cast this, @@ -1319,11 +1319,11 @@ begin cardinal.mk_fintype, lift_nat_cast, lift_nat_cast, nat_cast_inj] at this, end -lemma finrank_span_set_eq_card (s : set V) [fin : fintype s] +lemma finrank_span_set_eq_card (s : set V) [fintype s] (hs : linear_independent K (coe : s → V)) : finrank K (span K s) = s.to_finset.card := begin - haveI := span_of_finite K ⟨fin⟩, + haveI := span_of_finite K (set.finite_of_fintype s), have : module.rank K (span K s) = #s := dim_span_set hs, rw [←finrank_eq_dim, cardinal.mk_fintype, ←set.to_finset_card] at this, exact_mod_cast this, diff --git a/src/linear_algebra/linear_independent.lean b/src/linear_algebra/linear_independent.lean index ea16883d14a51..fce666ca2786d 100644 --- a/src/linear_algebra/linear_independent.lean +++ b/src/linear_algebra/linear_independent.lean @@ -383,7 +383,7 @@ begin end lemma linear_independent_of_finite (s : set M) - (H : ∀ t ⊆ s, finite t → linear_independent R (λ x, x : t → M)) : + (H : ∀ t ⊆ s, set.finite t → linear_independent R (λ x, x : t → M)) : linear_independent R (λ x, x : s → M) := linear_independent_subtype.2 $ λ l hl, linear_independent_subtype.1 (H _ hl (finset.finite_to_set _)) l (subset.refl _) @@ -643,7 +643,7 @@ lemma linear_independent.union {s t : set M} lemma linear_independent_Union_finite_subtype {ι : Type*} {f : ι → set M} (hl : ∀i, linear_independent R (λ x, x : f i → M)) - (hd : ∀i, ∀t:set ι, finite t → i ∉ t → disjoint (span R (f i)) (⨆i∈t, span R (f i))) : + (hd : ∀i, ∀t:set ι, t.finite → i ∉ t → disjoint (span R (f i)) (⨆i∈t, span R (f i))) : linear_independent R (λ x, x : (⋃i, f i) → M) := begin rw [Union_eq_Union_finset f], @@ -663,7 +663,7 @@ end lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*} {f : Π j : η, ιs j → M} (hindep : ∀j, linear_independent R (f j)) - (hd : ∀i, ∀t:set η, finite t → i ∉ t → + (hd : ∀i, ∀t:set η, t.finite → i ∉ t → disjoint (span R (range (f i))) (⨆i∈t, span R (range (f i)))) : linear_independent R (λ ji : Σ j, ιs j, f ji.1 ji.2) := begin @@ -1271,11 +1271,11 @@ begin end lemma exists_finite_card_le_of_finite_of_linear_independent_of_span - (ht : finite t) (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ span K t) : - ∃h : finite s, h.to_finset.card ≤ ht.to_finset.card := + (ht : t.finite) (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ span K t) : + ∃h : s.finite, h.to_finset.card ≤ ht.to_finset.card := have s ⊆ (span K ↑(ht.to_finset) : submodule K V), by simp; assumption, let ⟨u, hust, hsu, eq⟩ := exists_of_linear_independent_of_finite_span hs this in -have finite s, from u.finite_to_set.subset hsu, +have s.finite, from u.finite_to_set.subset hsu, ⟨this, by rw [←eq]; exact (finset.card_le_of_subset $ finset.coe_subset.mp $ by simp [hsu])⟩ end module diff --git a/src/measure_theory/integral/integrable_on.lean b/src/measure_theory/integral/integrable_on.lean index 718067b12b7ec..2ddc288a500f2 100644 --- a/src/measure_theory/integral/integrable_on.lean +++ b/src/measure_theory/integral/integrable_on.lean @@ -157,7 +157,7 @@ begin simp, end -@[simp] lemma integrable_on_finite_Union {s : set β} (hs : finite s) +@[simp] lemma integrable_on_finite_Union {s : set β} (hs : s.finite) {t : β → set α} : integrable_on f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, integrable_on f (t i) μ := begin apply hs.induction_on, diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index 0166f2316a3d4..23eed59851bf2 100644 --- a/src/measure_theory/measurable_space.lean +++ b/src/measure_theory/measurable_space.lean @@ -458,7 +458,7 @@ lemma measurable.dite [∀ x, decidable (x ∈ s)] {f : s → β} (hf : measurab measurable_of_restrict_of_restrict_compl hs (by simpa) (by simpa) lemma measurable_of_measurable_on_compl_finite [measurable_singleton_class α] - {f : α → β} (s : set α) (hs : finite s) (hf : measurable (sᶜ.restrict f)) : + {f : α → β} (s : set α) (hs : s.finite) (hf : measurable (sᶜ.restrict f)) : measurable f := begin letI : fintype s := finite.fintype hs, diff --git a/src/measure_theory/measurable_space_def.lean b/src/measure_theory/measurable_space_def.lean index c7cf0139715b6..ec369295a4eb5 100644 --- a/src/measure_theory/measurable_space_def.lean +++ b/src/measure_theory/measurable_space_def.lean @@ -110,7 +110,7 @@ begin exact measurable_set.Union (by simpa using h) end -lemma set.finite.measurable_set_bUnion {f : β → set α} {s : set β} (hs : finite s) +lemma set.finite.measurable_set_bUnion {f : β → set α} {s : set β} (hs : s.finite) (h : ∀ b ∈ s, measurable_set (f b)) : measurable_set (⋃ b ∈ s, f b) := measurable_set.bUnion hs.countable h @@ -124,7 +124,7 @@ lemma measurable_set.sUnion {s : set (set α)} (hs : countable s) (h : ∀ t ∈ measurable_set (⋃₀ s) := by { rw sUnion_eq_bUnion, exact measurable_set.bUnion hs h } -lemma set.finite.measurable_set_sUnion {s : set (set α)} (hs : finite s) +lemma set.finite.measurable_set_sUnion {s : set (set α)} (hs : s.finite) (h : ∀ t ∈ s, measurable_set t) : measurable_set (⋃₀ s) := measurable_set.sUnion hs.countable h @@ -157,7 +157,7 @@ lemma measurable_set.bInter {f : β → set α} {s : set β} (hs : countable s) measurable_set.compl_iff.1 $ by { rw compl_Inter₂, exact measurable_set.bUnion hs (λ b hb, (h b hb).compl) } -lemma set.finite.measurable_set_bInter {f : β → set α} {s : set β} (hs : finite s) +lemma set.finite.measurable_set_bInter {f : β → set α} {s : set β} (hs : s.finite) (h : ∀ b ∈ s, measurable_set (f b)) : measurable_set (⋂ b ∈ s, f b) := measurable_set.bInter hs.countable h @@ -169,7 +169,7 @@ lemma measurable_set.sInter {s : set (set α)} (hs : countable s) (h : ∀ t ∈ measurable_set (⋂₀ s) := by { rw sInter_eq_bInter, exact measurable_set.bInter hs h } -lemma set.finite.measurable_set_sInter {s : set (set α)} (hs : finite s) +lemma set.finite.measurable_set_sInter {s : set (set α)} (hs : s.finite) (h : ∀ t ∈ s, measurable_set t) : measurable_set (⋂₀ s) := measurable_set.sInter hs.countable h @@ -257,7 +257,7 @@ lemma measurable_set.insert {s : set α} (hs : measurable_set s) (a : α) : lemma set.subsingleton.measurable_set {s : set α} (hs : s.subsingleton) : measurable_set s := hs.induction_on measurable_set.empty measurable_set_singleton -lemma set.finite.measurable_set {s : set α} (hs : finite s) : measurable_set s := +lemma set.finite.measurable_set {s : set α} (hs : s.finite) : measurable_set s := finite.induction_on hs measurable_set.empty $ λ a s ha hsf hsm, hsm.insert _ protected lemma finset.measurable_set (s : finset α) : measurable_set (↑s : set α) := diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 64ebfa6e04c55..27657aa96cd3c 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -1648,7 +1648,7 @@ calc count (↑s : set α) = ∑' i : (↑s : set α), 1 : count_apply s.measura ... = ∑ i in s, 1 : s.tsum_subtype 1 ... = s.card : by simp -lemma count_apply_finite [measurable_singleton_class α] (s : set α) (hs : finite s) : +lemma count_apply_finite [measurable_singleton_class α] (s : set α) (hs : s.finite) : count s = hs.to_finset.card := by rw [← count_apply_finset, finite.coe_to_finset] diff --git a/src/measure_theory/measure/measure_space_def.lean b/src/measure_theory/measure/measure_space_def.lean index 6868f5d4042af..38a8263742957 100644 --- a/src/measure_theory/measure/measure_space_def.lean +++ b/src/measure_theory/measure/measure_space_def.lean @@ -214,7 +214,7 @@ lemma measure_Union_fintype_le [fintype β] (f : β → set α) : μ (⋃ b, f b) ≤ ∑ p, μ (f p) := by { convert measure_bUnion_finset_le finset.univ f, simp } -lemma measure_bUnion_lt_top {s : set β} {f : β → set α} (hs : finite s) +lemma measure_bUnion_lt_top {s : set β} {f : β → set α} (hs : s.finite) (hfin : ∀ i ∈ s, μ (f i) ≠ ∞) : μ (⋃ i ∈ s, f i) < ∞ := begin convert (measure_bUnion_finset_le hs.to_finset f).trans_lt _, diff --git a/src/measure_theory/measure/null_measurable.lean b/src/measure_theory/measure/null_measurable.lean index f64dcb5ca470d..085d50f49a9bc 100644 --- a/src/measure_theory/measure/null_measurable.lean +++ b/src/measure_theory/measure/null_measurable.lean @@ -308,7 +308,7 @@ measurable_set_insert lemma null_measurable_set_eq {a : α} : null_measurable_set {x | x = a} μ := null_measurable_set_singleton a -protected lemma _root_.set.finite.null_measurable_set (hs : finite s) : null_measurable_set s μ := +protected lemma _root_.set.finite.null_measurable_set (hs : s.finite) : null_measurable_set s μ := finite.measurable_set hs protected lemma _root_.finset.null_measurable_set (s : finset α) : null_measurable_set ↑s μ := @@ -316,7 +316,7 @@ finset.measurable_set s end measurable_singleton_class -lemma _root_.set.finite.null_measurable_set_bUnion {f : ι → set α} {s : set ι} (hs : finite s) +lemma _root_.set.finite.null_measurable_set_bUnion {f : ι → set α} {s : set ι} (hs : s.finite) (h : ∀ b ∈ s, null_measurable_set (f b) μ) : null_measurable_set (⋃ b ∈ s, f b) μ := finite.measurable_set_bUnion hs h @@ -326,12 +326,12 @@ lemma _root_.finset.null_measurable_set_bUnion {f : ι → set α} (s : finset null_measurable_set (⋃ b ∈ s, f b) μ := finset.measurable_set_bUnion s h -lemma _root_.set.finite.null_measurable_set_sUnion {s : set (set α)} (hs : finite s) +lemma _root_.set.finite.null_measurable_set_sUnion {s : set (set α)} (hs : s.finite) (h : ∀ t ∈ s, null_measurable_set t μ) : null_measurable_set (⋃₀ s) μ := finite.measurable_set_sUnion hs h -lemma _root_.set.finite.null_measurable_set_bInter {f : ι → set α} {s : set ι} (hs : finite s) +lemma _root_.set.finite.null_measurable_set_bInter {f : ι → set α} {s : set ι} (hs : s.finite) (h : ∀ b ∈ s, null_measurable_set (f b) μ) : null_measurable_set (⋂ b ∈ s, f b) μ := finite.measurable_set_bInter hs h @@ -339,7 +339,7 @@ lemma _root_.finset.null_measurable_set_bInter {f : ι → set α} (s : finset (h : ∀ b ∈ s, null_measurable_set (f b) μ) : null_measurable_set (⋂ b ∈ s, f b) μ := s.finite_to_set.null_measurable_set_bInter h -lemma _root_.set.finite.null_measurable_set_sInter {s : set (set α)} (hs : finite s) +lemma _root_.set.finite.null_measurable_set_sInter {s : set (set α)} (hs : s.finite) (h : ∀ t ∈ s, null_measurable_set t μ) : null_measurable_set (⋂₀ s) μ := null_measurable_set.sInter hs.countable h diff --git a/src/model_theory/finitely_generated.lean b/src/model_theory/finitely_generated.lean index 1ce88447d7115..dce01734c2433 100644 --- a/src/model_theory/finitely_generated.lean +++ b/src/model_theory/finitely_generated.lean @@ -60,7 +60,7 @@ end theorem fg_bot : (⊥ : L.substructure M).fg := ⟨∅, by rw [finset.coe_empty, closure_empty]⟩ -theorem fg_closure {s : set M} (hs : finite s) : fg (closure L s) := +theorem fg_closure {s : set M} (hs : s.finite) : fg (closure L s) := ⟨hs.to_finset, by rw [hs.coe_to_finset]⟩ theorem fg_closure_singleton (x : M) : fg (closure L ({x} : set M)) := diff --git a/src/order/conditionally_complete_lattice.lean b/src/order/conditionally_complete_lattice.lean index 5f9db654fdeea..c321dd46e115e 100644 --- a/src/order/conditionally_complete_lattice.lean +++ b/src/order/conditionally_complete_lattice.lean @@ -589,16 +589,16 @@ by { rw h.cSup_eq_max', exact s.max'_mem _ } lemma finset.nonempty.cInf_mem {s : finset α} (h : s.nonempty) : Inf (s : set α) ∈ s := @finset.nonempty.cSup_mem αᵒᵈ _ _ h -lemma set.nonempty.cSup_mem (h : s.nonempty) (hs : finite s) : Sup s ∈ s := +lemma set.nonempty.cSup_mem (h : s.nonempty) (hs : s.finite) : Sup s ∈ s := by { lift s to finset α using hs, exact finset.nonempty.cSup_mem h } -lemma set.nonempty.cInf_mem (h : s.nonempty) (hs : finite s) : Inf s ∈ s := +lemma set.nonempty.cInf_mem (h : s.nonempty) (hs : s.finite) : Inf s ∈ s := @set.nonempty.cSup_mem αᵒᵈ _ _ h hs -lemma set.finite.cSup_lt_iff (hs : finite s) (h : s.nonempty) : Sup s < a ↔ ∀ x ∈ s, x < a := +lemma set.finite.cSup_lt_iff (hs : s.finite) (h : s.nonempty) : Sup s < a ↔ ∀ x ∈ s, x < a := ⟨λ h x hx, (le_cSup hs.bdd_above hx).trans_lt h, λ H, H _ $ h.cSup_mem hs⟩ -lemma set.finite.lt_cInf_iff (hs : finite s) (h : s.nonempty) : a < Inf s ↔ ∀ x ∈ s, a < x := +lemma set.finite.lt_cInf_iff (hs : s.finite) (h : s.nonempty) : a < Inf s ↔ ∀ x ∈ s, a < x := @set.finite.cSup_lt_iff αᵒᵈ _ _ _ hs h /-- When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean index 877fa897b4d0b..99a4a02b165bb 100644 --- a/src/order/filter/bases.lean +++ b/src/order/filter/bases.lean @@ -204,7 +204,7 @@ variables {l l' : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} {p' : ι' → Prop} {s' : ι' → set α} {i' : ι'} lemma has_basis_generate (s : set (set α)) : - (generate s).has_basis (λ t, finite t ∧ t ⊆ s) (λ t, ⋂₀ t) := + (generate s).has_basis (λ t, set.finite t ∧ t ⊆ s) (λ t, ⋂₀ t) := ⟨begin intro U, rw mem_generate_iff, @@ -214,7 +214,7 @@ end⟩ /-- The smallest filter basis containing a given collection of sets. -/ def filter_basis.of_sets (s : set (set α)) : filter_basis α := -{ sets := sInter '' { t | finite t ∧ t ⊆ s}, +{ sets := sInter '' { t | set.finite t ∧ t ⊆ s}, nonempty := ⟨univ, ∅, ⟨⟨finite_empty, empty_subset s⟩, sInter_empty⟩⟩, inter_sets := begin rintros _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩, @@ -276,7 +276,7 @@ lemma has_basis.eq_generate (h : l.has_basis p s) : l = generate { U | ∃ i, p by rw [← h.is_basis.filter_eq_generate, h.filter_eq] lemma generate_eq_generate_inter (s : set (set α)) : - generate s = generate (sInter '' { t | finite t ∧ t ⊆ s}) := + generate s = generate (sInter '' { t | set.finite t ∧ t ⊆ s}) := by erw [(filter_basis.of_sets s).generate, ← (has_basis_generate s).filter_eq] ; refl lemma of_sets_filter_eq_generate (s : set (set α)) : (filter_basis.of_sets s).filter = generate s := @@ -417,7 +417,7 @@ lemma has_basis.inf {ι ι' : Type*} {p : ι → Prop} {s : ι → set α} {p' : lemma has_basis_infi {ι : Sort*} {ι' : ι → Type*} {l : ι → filter α} {p : Π i, ι' i → Prop} {s : Π i, ι' i → set α} (hl : ∀ i, (l i).has_basis (p i) (s i)) : - (⨅ i, l i).has_basis (λ If : set ι × Π i, ι' i, finite If.1 ∧ ∀ i ∈ If.1, p i (If.2 i)) + (⨅ i, l i).has_basis (λ If : set ι × Π i, ι' i, If.1.finite ∧ ∀ i ∈ If.1, p i (If.2 i)) (λ If : set ι × Π i, ι' i, ⋂ i ∈ If.1, s i (If.2 i)) := ⟨begin intro t, @@ -560,7 +560,7 @@ end⟩ /-- If `s : ι → set α` is an indexed family of sets, then finite intersections of `s i` form a basis of `⨅ i, 𝓟 (s i)`. -/ lemma has_basis_infi_principal_finite {ι : Type*} (s : ι → set α) : - (⨅ i, 𝓟 (s i)).has_basis (λ t : set ι, finite t) (λ t, ⋂ i ∈ t, s i) := + (⨅ i, 𝓟 (s i)).has_basis (λ t : set ι, t.finite) (λ t, ⋂ i ∈ t, s i) := begin refine ⟨λ U, (mem_infi_finite _).trans _⟩, simp only [infi_principal_finset, mem_Union, mem_principal, exists_prop, diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 1360650ac4c4b..537c09a3782b8 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -150,7 +150,7 @@ lemma congr_sets (h : {x | x ∈ s ↔ x ∈ t} ∈ f) : s ∈ f ↔ t ∈ f := ⟨λ hs, mp_mem hs (mem_of_superset h (λ x, iff.mp)), λ hs, mp_mem hs (mem_of_superset h (λ x, iff.mpr))⟩ -@[simp] lemma bInter_mem {β : Type v} {s : β → set α} {is : set β} (hf : finite is) : +@[simp] lemma bInter_mem {β : Type v} {s : β → set α} {is : set β} (hf : is.finite) : (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := finite.induction_on hf (by simp) (λ i s hi _ hs, by simp [hs]) @@ -161,7 +161,7 @@ bInter_mem is.finite_to_set alias bInter_finset_mem ← finset.Inter_mem_sets attribute [protected] finset.Inter_mem_sets -@[simp] lemma sInter_mem {s : set (set α)} (hfin : finite s) : +@[simp] lemma sInter_mem {s : set (set α)} (hfin : s.finite) : ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f := by rw [sInter_eq_bInter, bInter_mem hfin] @@ -308,7 +308,7 @@ iff.intro (λ x y _ _ hx hy, inter_mem hx hy)) lemma mem_generate_iff {s : set $ set α} {U : set α} : - U ∈ generate s ↔ ∃ t ⊆ s, finite t ∧ ⋂₀ t ⊆ U := + U ∈ generate s ↔ ∃ t ⊆ s, set.finite t ∧ ⋂₀ t ⊆ U := begin split ; intro h, { induction h, @@ -510,7 +510,7 @@ show generate _ = generate _, from congr_arg _ $ congr_arg Sup $ (range_comp _ _ lemma mem_infi_of_mem {f : ι → filter α} (i : ι) : ∀ {s}, s ∈ f i → s ∈ ⨅ i, f i := show (⨅ i, f i) ≤ f i, from infi_le _ _ -lemma mem_infi_of_Inter {ι} {s : ι → filter α} {U : set α} {I : set ι} (I_fin : finite I) +lemma mem_infi_of_Inter {ι} {s : ι → filter α} {U : set α} {I : set ι} (I_fin : I.finite) {V : I → set α} (hV : ∀ i, V i ∈ s i) (hU : (⋂ i, V i) ⊆ U) : U ∈ ⨅ i, s i := begin haveI := I_fin.fintype, @@ -519,7 +519,7 @@ begin end lemma mem_infi {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔ - ∃ I : set ι, finite I ∧ ∃ V : I → set α, (∀ i, V i ∈ s i) ∧ U = ⋂ i, V i := + ∃ I : set ι, I.finite ∧ ∃ V : I → set α, (∀ i, V i ∈ s i) ∧ U = ⋂ i, V i := begin split, { rw [infi_eq_generate, mem_generate_iff], @@ -540,7 +540,7 @@ begin end lemma mem_infi' {ι} {s : ι → filter α} {U : set α} : (U ∈ ⨅ i, s i) ↔ - ∃ I : set ι, finite I ∧ ∃ V : ι → set α, (∀ i, V i ∈ s i) ∧ + ∃ I : set ι, I.finite ∧ ∃ V : ι → set α, (∀ i, V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ (U = ⋂ i ∈ I, V i) ∧ U = ⋂ i, V i := begin simp only [mem_infi, set_coe.forall', bInter_eq_Inter], @@ -897,7 +897,7 @@ end (⨅ i, 𝓟 (f i)) = 𝓟 (⋂ i, f i) := by simpa using infi_principal_finset finset.univ f -lemma infi_principal_finite {ι : Type w} {s : set ι} (hs : finite s) (f : ι → set α) : +lemma infi_principal_finite {ι : Type w} {s : set ι} (hs : s.finite) (f : ι → set α) : (⨅ i ∈ s, 𝓟 (f i)) = 𝓟 (⋂ i ∈ s, f i) := begin lift s to finset ι using hs, diff --git a/src/order/filter/cofinite.lean b/src/order/filter/cofinite.lean index 38f8908f2dec6..02f6be134ff89 100644 --- a/src/order/filter/cofinite.lean +++ b/src/order/filter/cofinite.lean @@ -29,17 +29,17 @@ namespace filter /-- The cofinite filter is the filter of subsets whose complements are finite. -/ def cofinite : filter α := -{ sets := {s | finite sᶜ}, +{ sets := {s | sᶜ.finite}, univ_sets := by simp only [compl_univ, finite_empty, mem_set_of_eq], - sets_of_superset := assume s t (hs : finite sᶜ) (st: s ⊆ t), + sets_of_superset := assume s t (hs : sᶜ.finite) (st: s ⊆ t), hs.subset $ compl_subset_compl.2 st, - inter_sets := assume s t (hs : finite sᶜ) (ht : finite (tᶜ)), + inter_sets := assume s t (hs : sᶜ.finite) (ht : tᶜ.finite), by simp only [compl_inter, finite.union, ht, hs, mem_set_of_eq] } -@[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ finite sᶜ := iff.rfl +@[simp] lemma mem_cofinite {s : set α} : s ∈ (@cofinite α) ↔ sᶜ.finite := iff.rfl @[simp] lemma eventually_cofinite {p : α → Prop} : - (∀ᶠ x in cofinite, p x) ↔ finite {x | ¬p x} := iff.rfl + (∀ᶠ x in cofinite, p x) ↔ {x | ¬p x}.finite := iff.rfl lemma has_basis_cofinite : has_basis cofinite (λ s : set α, s.finite) compl := ⟨λ s, ⟨λ h, ⟨sᶜ, h, (compl_compl s).subset⟩, λ ⟨t, htf, hts⟩, htf.subset $ compl_subset_comm.2 hts⟩⟩ @@ -123,7 +123,7 @@ lemma filter.tendsto.exists_within_forall_le {α β : Type*} [linear_order β] { begin rcases em (∃ y ∈ s, ∃ x, f y < x) with ⟨y, hys, x, hx⟩|not_all_top, { -- the set of points `{y | f y < x}` is nonempty and finite, so we take `min` over this set - have : finite {y | ¬x ≤ f y} := (filter.eventually_cofinite.mp (tendsto_at_top.1 hf x)), + have : {y | ¬x ≤ f y}.finite := (filter.eventually_cofinite.mp (tendsto_at_top.1 hf x)), simp only [not_le] at this, obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ := exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩, diff --git a/src/order/filter/pi.lean b/src/order/filter/pi.lean index 8ee93c4bcb42c..1557a4eeef974 100644 --- a/src/order/filter/pi.lean +++ b/src/order/filter/pi.lean @@ -47,7 +47,7 @@ lemma mem_pi_of_mem (i : ι) {s : set (α i)} (hs : s ∈ f i) : eval i ⁻¹' s ∈ pi f := mem_infi_of_mem i $ preimage_mem_comap hs -lemma pi_mem_pi {I : set ι} (hI : finite I) (h : ∀ i ∈ I, s i ∈ f i) : +lemma pi_mem_pi {I : set ι} (hI : I.finite) (h : ∀ i ∈ I, s i ∈ f i) : I.pi s ∈ pi f := begin rw [pi_def, bInter_eq_Inter], @@ -56,7 +56,7 @@ begin end lemma mem_pi {s : set (Π i, α i)} : s ∈ pi f ↔ - ∃ (I : set ι), finite I ∧ ∃ t : Π i, set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s := + ∃ (I : set ι), I.finite ∧ ∃ t : Π i, set (α i), (∀ i, t i ∈ f i) ∧ I.pi t ⊆ s := begin split, { simp only [pi, mem_infi', mem_comap, pi_def], @@ -82,13 +82,13 @@ begin simpa using hts this i hi end -@[simp] lemma pi_mem_pi_iff [∀ i, ne_bot (f i)] {I : set ι} (hI : finite I) : +@[simp] lemma pi_mem_pi_iff [∀ i, ne_bot (f i)] {I : set ι} (hI : I.finite) : I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i := ⟨λ h i hi, mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩ lemma has_basis_pi {ι' : ι → Type} {s : Π i, ι' i → set (α i)} {p : Π i, ι' i → Prop} (h : ∀ i, (f i).has_basis (p i) (s i)) : - (pi f).has_basis (λ If : set ι × Π i, ι' i, finite If.1 ∧ ∀ i ∈ If.1, p i (If.2 i)) + (pi f).has_basis (λ If : set ι × Π i, ι' i, If.1.finite ∧ ∀ i ∈ If.1, p i (If.2 i)) (λ If : set ι × Π i, ι' i, If.1.pi (λ i, s i $ If.2 i)) := begin have : (pi f).has_basis _ _ := has_basis_infi (λ i, (h i).comap (eval i : (Π j, α j) → α i)), diff --git a/src/order/filter/ultrafilter.lean b/src/order/filter/ultrafilter.lean index e7cf01a03f8e2..66766e9a78da1 100644 --- a/src/order/filter/ultrafilter.lean +++ b/src/order/filter/ultrafilter.lean @@ -110,11 +110,11 @@ lemma eventually_not : (∀ᶠ x in f, ¬p x) ↔ ¬∀ᶠ x in f, p x := compl_ lemma eventually_imp : (∀ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∀ᶠ x in f, q x := by simp only [imp_iff_not_or, eventually_or, eventually_not] -lemma finite_sUnion_mem_iff {s : set (set α)} (hs : finite s) : ⋃₀ s ∈ f ↔ ∃t∈s, t ∈ f := +lemma finite_sUnion_mem_iff {s : set (set α)} (hs : s.finite) : ⋃₀ s ∈ f ↔ ∃t∈s, t ∈ f := finite.induction_on hs (by simp) $ λ a s ha hs his, by simp [union_mem_iff, his, or_and_distrib_right, exists_or_distrib] -lemma finite_bUnion_mem_iff {is : set β} {s : β → set α} (his : finite is) : +lemma finite_bUnion_mem_iff {is : set β} {s : β → set α} (his : is.finite) : (⋃i∈is, s i) ∈ f ↔ ∃i∈is, s i ∈ f := by simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), bex_image_iff] diff --git a/src/order/locally_finite.lean b/src/order/locally_finite.lean index 54634155c3da1..0e10502cacd28 100644 --- a/src/order/locally_finite.lean +++ b/src/order/locally_finite.lean @@ -327,10 +327,10 @@ fintype.of_finset (finset.Ioc a b) (λ x, by rw [finset.mem_Ioc, mem_Ioc]) instance fintype_Ioo : fintype (Ioo a b) := fintype.of_finset (finset.Ioo a b) (λ x, by rw [finset.mem_Ioo, mem_Ioo]) -lemma finite_Icc : (Icc a b).finite := ⟨set.fintype_Icc a b⟩ -lemma finite_Ico : (Ico a b).finite := ⟨set.fintype_Ico a b⟩ -lemma finite_Ioc : (Ioc a b).finite := ⟨set.fintype_Ioc a b⟩ -lemma finite_Ioo : (Ioo a b).finite := ⟨set.fintype_Ioo a b⟩ +lemma finite_Icc : (Icc a b).finite := set.finite_of_fintype _ +lemma finite_Ico : (Ico a b).finite := set.finite_of_fintype _ +lemma finite_Ioc : (Ioc a b).finite := set.finite_of_fintype _ +lemma finite_Ioo : (Ioo a b).finite := set.finite_of_fintype _ end preorder @@ -343,8 +343,8 @@ fintype.of_finset (finset.Ici a) (λ x, by rw [finset.mem_Ici, mem_Ici]) instance fintype_Ioi : fintype (Ioi a) := fintype.of_finset (finset.Ioi a) (λ x, by rw [finset.mem_Ioi, mem_Ioi]) -lemma finite_Ici : (Ici a).finite := ⟨set.fintype_Ici a⟩ -lemma finite_Ioi : (Ioi a).finite := ⟨set.fintype_Ioi a⟩ +lemma finite_Ici : (Ici a).finite := set.finite_of_fintype _ +lemma finite_Ioi : (Ioi a).finite := set.finite_of_fintype _ end order_top @@ -357,8 +357,8 @@ fintype.of_finset (finset.Iic b) (λ x, by rw [finset.mem_Iic, mem_Iic]) instance fintype_Iio : fintype (Iio b) := fintype.of_finset (finset.Iio b) (λ x, by rw [finset.mem_Iio, mem_Iio]) -lemma finite_Iic : (Iic b).finite := ⟨set.fintype_Iic b⟩ -lemma finite_Iio : (Iio b).finite := ⟨set.fintype_Iio b⟩ +lemma finite_Iic : (Iic b).finite := set.finite_of_fintype _ +lemma finite_Iio : (Iio b).finite := set.finite_of_fintype _ end order_bot diff --git a/src/ring_theory/algebraic_independent.lean b/src/ring_theory/algebraic_independent.lean index 9b7ef29765d7c..0ee9b87995b14 100644 --- a/src/ring_theory/algebraic_independent.lean +++ b/src/ring_theory/algebraic_independent.lean @@ -278,7 +278,7 @@ theorem algebraic_independent_subtype {s : set A} : by apply @algebraic_independent_comp_subtype _ _ _ id lemma algebraic_independent_of_finite (s : set A) - (H : ∀ t ⊆ s, finite t → algebraic_independent R (λ x, x : t → A)) : + (H : ∀ t ⊆ s, t.finite → algebraic_independent R (λ x, x : t → A)) : algebraic_independent R (λ x, x : s → A) := algebraic_independent_subtype.2 $ λ p hp, algebraic_independent_subtype.1 (H _ (mem_supported.1 hp) (finset.finite_to_set _)) _ diff --git a/src/ring_theory/artinian.lean b/src/ring_theory/artinian.lean index abf1163b11ab4..06cf78f81578d 100644 --- a/src/ring_theory/artinian.lean +++ b/src/ring_theory/artinian.lean @@ -165,7 +165,7 @@ lemma is_artinian.finite_of_linear_independent [nontrivial R] [is_artinian R M] begin refine classical.by_contradiction (λ hf, (rel_embedding.well_founded_iff_no_descending_seq.1 (well_founded_submodule_lt R M)).elim' _), - have f : ℕ ↪ s, from @infinite.nat_embedding s ⟨λ f, hf ⟨f⟩⟩, + have f : ℕ ↪ s, from set.infinite.nat_embedding s hf, have : ∀ n, (coe ∘ f) '' {m | n ≤ m} ⊆ s, { rintros n x ⟨y, hy₁, rfl⟩, exact (f y).2 }, have : ∀ a b : ℕ, a ≤ b ↔ @@ -368,7 +368,7 @@ by exactI is_artinian_of_linear_equiv (linear_equiv.of_top (⊤ : submodule R M) /-- In a module over a artinian ring, the submodule generated by finitely many vectors is artinian. -/ theorem is_artinian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R M] - [is_artinian_ring R] {A : set M} (hA : finite A) : is_artinian R (submodule.span R A) := + [is_artinian_ring R] {A : set M} (hA : A.finite) : is_artinian R (submodule.span R A) := is_artinian_of_fg_of_artinian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩) theorem is_artinian_ring_of_surjective (R) [ring R] (S) [ring S] diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean index da2624f14ecb2..994b269f96b2a 100644 --- a/src/ring_theory/noetherian.lean +++ b/src/ring_theory/noetherian.lean @@ -68,7 +68,7 @@ variables {R : Type*} {M : Type*} [semiring R] [add_comm_monoid M] [module R M] def fg (N : submodule R M) : Prop := ∃ S : finset M, submodule.span R ↑S = N theorem fg_def {N : submodule R M} : - N.fg ↔ ∃ S : set M, finite S ∧ span R S = N := + N.fg ↔ ∃ S : set M, S.finite ∧ span R S = N := ⟨λ ⟨t, h⟩, ⟨_, finset.finite_to_set t, h⟩, begin rintro ⟨t', h, rfl⟩, rcases finite.exists_finset_coe h with ⟨t, rfl⟩, @@ -143,7 +143,7 @@ lemma _root_.subalgebra.fg_bot_to_submodule {R A : Type*} (⊥ : subalgebra R A).to_submodule.fg := ⟨{1}, by simp [algebra.to_submodule_bot] ⟩ -theorem fg_span {s : set M} (hs : finite s) : fg (span R s) := +theorem fg_span {s : set M} (hs : s.finite) : fg (span R s) := ⟨hs.to_finset, by rw [hs.coe_to_finset]⟩ theorem fg_span_singleton (x : M) : fg (R ∙ x) := @@ -543,7 +543,7 @@ lemma finite_of_linear_independent [nontrivial R] [is_noetherian R M] begin refine classical.by_contradiction (λ hf, (rel_embedding.well_founded_iff_no_descending_seq.1 (well_founded_submodule_gt R M)).elim' _), - have f : ℕ ↪ s, from @infinite.nat_embedding s ⟨λ f, hf ⟨f⟩⟩, + have f : ℕ ↪ s, from set.infinite.nat_embedding s hf, have : ∀ n, (coe ∘ f) '' {m | m ≤ n} ⊆ s, { rintros n x ⟨y, hy₁, rfl⟩, exact (f y).2 }, have : ∀ a b : ℕ, a ≤ b ↔ @@ -758,7 +758,7 @@ by exactI is_noetherian_of_linear_equiv (linear_equiv.of_top (⊤ : submodule R /-- In a module over a noetherian ring, the submodule generated by finitely many vectors is noetherian. -/ theorem is_noetherian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R M] - [is_noetherian_ring R] {A : set M} (hA : finite A) : is_noetherian R (submodule.span R A) := + [is_noetherian_ring R] {A : set M} (hA : A.finite) : is_noetherian R (submodule.span R A) := is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩) theorem is_noetherian_ring_of_surjective (R) [ring R] (S) [ring S] diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index 68b634cdbbfc6..6c3d49288dc90 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -906,7 +906,7 @@ theorem lt_omega {c : cardinal.{u}} : c < ω ↔ ∃ n : ℕ, c = n := ⟨λ h, begin rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩, rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩, - suffices : finite S, + suffices : S.finite, { lift S to finset ℕ using this, simp }, contrapose! h', @@ -931,7 +931,7 @@ end, λ ⟨_⟩, by exactI ⟨_, mk_fintype _⟩⟩ theorem lt_omega_of_fintype (α : Type u) [fintype α] : #α < ω := lt_omega_iff_fintype.2 ⟨infer_instance⟩ -theorem lt_omega_iff_finite {α} {S : set α} : #S < ω ↔ finite S := +theorem lt_omega_iff_finite {α} {S : set α} : #S < ω ↔ S.finite := lt_omega_iff_fintype.trans finite_def.symm instance can_lift_cardinal_nat : can_lift cardinal ℕ := diff --git a/src/topology/G_delta.lean b/src/topology/G_delta.lean index 76a6e6206bae1..353e6608e64c0 100644 --- a/src/topology/G_delta.lean +++ b/src/topology/G_delta.lean @@ -128,7 +128,7 @@ begin exact is_Gδ_bInter hs (λ x _, is_Gδ_compl_singleton x) end -lemma set.finite.is_Gδ_compl {s : set α} (hs : finite s) : is_Gδ sᶜ := +lemma set.finite.is_Gδ_compl {s : set α} (hs : s.finite) : is_Gδ sᶜ := hs.countable.is_Gδ_compl lemma set.subsingleton.is_Gδ_compl {s : set α} (hs : s.subsingleton) : is_Gδ sᶜ := @@ -148,7 +148,7 @@ begin exact is_Gδ_bInter (countable_encodable _) (λ n hn, (hU n).2.is_Gδ), end -lemma set.finite.is_Gδ {s : set α} (hs : finite s) : is_Gδ s := +lemma set.finite.is_Gδ {s : set α} (hs : s.finite) : is_Gδ s := finite.induction_on hs is_Gδ_empty $ λ a s _ _ hs, (is_Gδ_singleton a).union hs end t1_space diff --git a/src/topology/bases.lean b/src/topology/bases.lean index 7c83edd7206ab..b77db5377d228 100644 --- a/src/topology/bases.lean +++ b/src/topology/bases.lean @@ -66,7 +66,7 @@ structure is_topological_basis (s : set (set α)) : Prop := /-- If a family of sets `s` generates the topology, then nonempty intersections of finite subcollections of `s` form a topological basis. -/ lemma is_topological_basis_of_subbasis {s : set (set α)} (hs : t = generate_from s) : - is_topological_basis ((λ f, ⋂₀ f) '' {f : set (set α) | finite f ∧ f ⊆ s ∧ (⋂₀ f).nonempty}) := + is_topological_basis ((λ f, ⋂₀ f) '' {f : set (set α) | f.finite ∧ f ⊆ s ∧ (⋂₀ f).nonempty}) := begin refine ⟨_, _, _⟩, { rintro _ ⟨t₁, ⟨hft₁, ht₁b, ht₁⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b, ht₂⟩, rfl⟩ x h, @@ -363,7 +363,7 @@ end lemma _root_.set.countable.is_separable {s : set α} (hs : countable s) : is_separable s := ⟨s, hs, subset_closure⟩ -lemma _root_.set.finite.is_separable {s : set α} (hs : finite s) : is_separable s := +lemma _root_.set.finite.is_separable {s : set α} (hs : s.finite) : is_separable s := hs.countable.is_separable lemma is_separable_univ_iff : @@ -553,7 +553,7 @@ variable (α) lemma exists_countable_basis [second_countable_topology α] : ∃b:set (set α), countable b ∧ ∅ ∉ b ∧ is_topological_basis b := let ⟨b, hb₁, hb₂⟩ := second_countable_topology.is_open_generated_countable α in -let b' := (λs, ⋂₀ s) '' {s:set (set α) | finite s ∧ s ⊆ b ∧ (⋂₀ s).nonempty} in +let b' := (λs, ⋂₀ s) '' {s:set (set α) | s.finite ∧ s ⊆ b ∧ (⋂₀ s).nonempty} in ⟨b', ((countable_set_of_finite_subset hb₁).mono (by { simp only [← and_assoc], apply inter_subset_left })).image _, diff --git a/src/topology/basic.lean b/src/topology/basic.lean index 4a132ed51f3a9..d71ef9f7b82eb 100644 --- a/src/topology/basic.lean +++ b/src/topology/basic.lean @@ -129,12 +129,12 @@ by rw union_eq_Union; exact is_open_Union (bool.forall_bool.2 ⟨h₂, h₁⟩) @[simp] lemma is_open_empty : is_open (∅ : set α) := by rw ← sUnion_empty; exact is_open_sUnion (assume a, false.elim) -lemma is_open_sInter {s : set (set α)} (hs : finite s) : (∀t ∈ s, is_open t) → is_open (⋂₀ s) := +lemma is_open_sInter {s : set (set α)} (hs : s.finite) : (∀t ∈ s, is_open t) → is_open (⋂₀ s) := finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $ λ a s has hs ih h, by rw sInter_insert; exact is_open.inter (h _ $ mem_insert _ _) (ih $ λ t, h t ∘ mem_insert_of_mem _) -lemma is_open_bInter {s : set β} {f : β → set α} (hs : finite s) : +lemma is_open_bInter {s : set β} {f : β → set α} (hs : s.finite) : (∀i∈s, is_open (f i)) → is_open (⋂i∈s, f i) := finite.induction_on hs (λ _, by rw bInter_empty; exact is_open_univ) @@ -199,7 +199,7 @@ by { rw [← is_open_compl_iff] at *, rw compl_inter, exact is_open.union h₁ h lemma is_closed.sdiff {s t : set α} (h₁ : is_closed s) (h₂ : is_open t) : is_closed (s \ t) := is_closed.inter h₁ (is_closed_compl_iff.mpr h₂) -lemma is_closed_bUnion {s : set β} {f : β → set α} (hs : finite s) : +lemma is_closed_bUnion {s : set β} {f : β → set α} (hs : s.finite) : (∀i∈s, is_closed (f i)) → is_closed (⋃i∈s, f i) := finite.induction_on hs (λ _, by rw bUnion_empty; exact is_closed_empty) @@ -1184,10 +1184,10 @@ section locally_finite /-- A family of sets in `set α` is locally finite if at every point `x:α`, there is a neighborhood of `x` which meets only finitely many sets in the family -/ def locally_finite (f : β → set α) := -∀x:α, ∃t ∈ 𝓝 x, finite {i | (f i ∩ t).nonempty } +∀x:α, ∃t ∈ 𝓝 x, {i | (f i ∩ t).nonempty}.finite lemma locally_finite.point_finite {f : β → set α} (hf : locally_finite f) (x : α) : - finite {b | x ∈ f b} := + {b | x ∈ f b}.finite := let ⟨t, hxt, ht⟩ := hf x in ht.subset $ λ b hb, ⟨x, hb, mem_of_mem_nhds hxt⟩ lemma locally_finite_of_fintype [fintype β] (f : β → set α) : locally_finite f := diff --git a/src/topology/bornology/basic.lean b/src/topology/bornology/basic.lean index c3aeef4234909..2330825481f13 100644 --- a/src/topology/bornology/basic.lean +++ b/src/topology/bornology/basic.lean @@ -168,7 +168,7 @@ by rw [is_bounded_def, ←filter.mem_sets, of_bounded_cobounded_sets, set.mem_se variables [bornology α] -lemma is_cobounded_bInter {s : set ι} {f : ι → set α} (hs : finite s) : +lemma is_cobounded_bInter {s : set ι} {f : ι → set α} (hs : s.finite) : is_cobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, is_cobounded (f i) := bInter_mem hs @@ -180,11 +180,11 @@ bInter_finset_mem s is_cobounded (⋂ i, f i) ↔ ∀ i, is_cobounded (f i) := Inter_mem -lemma is_cobounded_sInter {S : set (set α)} (hs : finite S) : +lemma is_cobounded_sInter {S : set (set α)} (hs : S.finite) : is_cobounded (⋂₀ S) ↔ ∀ s ∈ S, is_cobounded s := sInter_mem hs -lemma is_bounded_bUnion {s : set ι} {f : ι → set α} (hs : finite s) : +lemma is_bounded_bUnion {s : set ι} {f : ι → set α} (hs : s.finite) : is_bounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, is_bounded (f i) := by simp only [← is_cobounded_compl_iff, compl_Union, is_cobounded_bInter hs] @@ -192,7 +192,7 @@ lemma is_bounded_bUnion_finset (s : finset ι) {f : ι → set α} : is_bounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, is_bounded (f i) := is_bounded_bUnion s.finite_to_set -lemma is_bounded_sUnion {S : set (set α)} (hs : finite S) : +lemma is_bounded_sUnion {S : set (set α)} (hs : S.finite) : is_bounded (⋃₀ S) ↔ (∀ s ∈ S, is_bounded s) := by rw [sUnion_eq_bUnion, is_bounded_bUnion hs] diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean index 12f3bc9a2658f..d5dcfbaa418a0 100644 --- a/src/topology/constructions.lean +++ b/src/topology/constructions.lean @@ -948,7 +948,7 @@ lemma continuous.fin_insert_nth {n} {π : fin (n + 1) → Type*} [Π i, topologi continuous_iff_continuous_at.2 $ λ a, hf.continuous_at.fin_insert_nth i hg.continuous_at lemma is_open_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set (π a)} - (hi : finite i) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) := + (hi : i.finite) (hs : ∀a∈i, is_open (s a)) : is_open (pi i s) := by rw [pi_def]; exact (is_open_bInter hi $ assume a ha, (hs _ ha).preimage (continuous_apply _)) lemma is_closed_set_pi [∀a, topological_space (π a)] {i : set ι} {s : Πa, set (π a)} @@ -962,7 +962,7 @@ lemma mem_nhds_of_pi_mem_nhds {ι : Type*} {α : ι → Type*} [Π (i : ι), top by { rw nhds_pi at hs, exact mem_of_pi_mem_pi hs hi } 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)) : + {x : Π a, π a} (hi : i.finite) (hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)) : pi i s ∈ 𝓝 x := by { rw [pi_def, bInter_mem hi], exact λ a ha, (continuous_apply a).continuous_at (hs a ha) } diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean index f1389ed2d36b8..15958affeb5b3 100644 --- a/src/topology/continuous_on.lean +++ b/src/topology/continuous_on.lean @@ -237,13 +237,13 @@ lemma nhds_within_prod {α : Type*} [topological_space α] {β : Type*} [topolog by { rw nhds_within_prod_eq, exact prod_mem_prod hu hv, } lemma nhds_within_pi_eq' {ι : Type*} {α : ι → Type*} [Π i, topological_space (α i)] - {I : set ι} (hI : finite I) (s : Π i, set (α i)) (x : Π i, α i) : + {I : set ι} (hI : I.finite) (s : Π i, set (α i)) (x : Π i, α i) : 𝓝[pi I s] x = ⨅ i, comap (λ x, x i) (𝓝 (x i) ⊓ ⨅ (hi : i ∈ I), 𝓟 (s i)) := by simp only [nhds_within, nhds_pi, filter.pi, comap_inf, comap_infi, pi_def, comap_principal, ← infi_principal_finite hI, ← infi_inf_eq] lemma nhds_within_pi_eq {ι : Type*} {α : ι → Type*} [Π i, topological_space (α i)] - {I : set ι} (hI : finite I) (s : Π i, set (α i)) (x : Π i, α i) : + {I : set ι} (hI : I.finite) (s : Π i, set (α i)) (x : Π i, α i) : 𝓝[pi I s] x = (⨅ i ∈ I, comap (λ x, x i) (𝓝[s i] (x i))) ⊓ ⨅ (i ∉ I), comap (λ x, x i) (𝓝 (x i)) := begin diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index c6aa0cec0f673..f44098dcf3c07 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -715,7 +715,7 @@ begin end theorem totally_bounded_iff {s : set α} : - totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε := + totally_bounded s ↔ ∀ ε > 0, ∃t : set α, t.finite ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, H _ (dist_mem_uniformity ε0), λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_dist.1 ru, ⟨t, ft, h⟩ := H ε ε0 in @@ -744,7 +744,7 @@ begin end theorem finite_approx_of_totally_bounded {s : set α} (hs : totally_bounded s) : - ∀ ε > 0, ∃ t ⊆ s, finite t ∧ s ⊆ ⋃y∈t, ball y ε := + ∀ ε > 0, ∃ t ⊆ s, set.finite t ∧ s ⊆ ⋃y∈t, ball y ε := begin intros ε ε_pos, rw totally_bounded_iff_subset at hs, @@ -1782,7 +1782,7 @@ section compact positive radius -/ lemma finite_cover_balls_of_compact {α : Type u} [pseudo_metric_space α] {s : set α} (hs : is_compact s) {e : ℝ} (he : 0 < e) : - ∃t ⊆ s, finite t ∧ s ⊆ ⋃x∈t, ball x e := + ∃t ⊆ s, set.finite t ∧ s ⊆ ⋃x∈t, ball x e := begin apply hs.elim_finite_subcover_image, { simp [is_open_ball] }, @@ -2054,7 +2054,7 @@ end ⟨λ h, ⟨h.mono (by simp), h.mono (by simp)⟩, λ h, h.1.union h.2⟩ /-- A finite union of bounded sets is bounded -/ -lemma bounded_bUnion {I : set β} {s : β → set α} (H : finite I) : +lemma bounded_bUnion {I : set β} {s : β → set α} (H : I.finite) : bounded (⋃i∈I, s i) ↔ ∀i ∈ I, bounded (s i) := finite.induction_on H (by simp) $ λ x I _ _ IH, by simp [or_imp_distrib, forall_and_distrib, IH] @@ -2085,7 +2085,7 @@ lemma _root_.is_compact.bounded {s : set α} (h : is_compact s) : bounded s := h.totally_bounded.bounded /-- A finite set is bounded -/ -lemma bounded_of_finite {s : set α} (h : finite s) : bounded s := +lemma bounded_of_finite {s : set α} (h : s.finite) : bounded s := h.is_compact.bounded alias bounded_of_finite ← set.finite.bounded @@ -2398,7 +2398,7 @@ lemma tendsto_coe_cofinite : tendsto (coe : ℤ → ℝ) cofinite (cocompact ℝ begin refine tendsto_cocompact_of_tendsto_dist_comp_at_top (0 : ℝ) _, simp only [filter.tendsto_at_top, eventually_cofinite, not_le, ← mem_ball], - change ∀ r : ℝ, finite (coe ⁻¹' (ball (0 : ℝ) r)), + change ∀ r : ℝ, (coe ⁻¹' (ball (0 : ℝ) r)).finite, simp [real.ball_eq_Ioo, set.finite_Ioo], end diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean index d47f80668a88b..244295b61f5cf 100644 --- a/src/topology/metric_space/closeds.lean +++ b/src/topology/metric_space/closeds.lean @@ -193,7 +193,7 @@ instance closeds.compact_space [compact_space α] : compact_space (closeds α) : rcases exists_between εpos with ⟨δ, δpos, δlt⟩, rcases emetric.totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 (@compact_univ α _ _)).1 δ δpos with ⟨s, fs, hs⟩, - -- s : set α, fs : finite s, hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ + -- s : set α, fs : s.finite, hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ -- we first show that any set is well approximated by a subset of `s`. have main : ∀ u : set α, ∃v ⊆ s, Hausdorff_edist u v ≤ δ, { assume u, @@ -271,7 +271,7 @@ begin rcases totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 ht.2).1 (ε/2) (ennreal.half_pos εpos.ne') with ⟨u, fu, ut⟩, refine ⟨u, ⟨fu, λx hx, _⟩⟩, - -- u : set α, fu : finite u, ut : t ⊆ ⋃ (y : α) (H : y ∈ u), eball y (ε / 2) + -- u : set α, fu : u.finite, ut : t ⊆ ⋃ (y : α) (H : y ∈ u), eball y (ε / 2) -- then s is covered by the union of the balls centered at u of radius ε rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dst with ⟨z, hz, Dxz⟩, rcases mem_Union₂.1 (ut hz) with ⟨y, hy, Dzy⟩, @@ -312,7 +312,7 @@ begin approximations in `s` of the centers of these balls give the required finite approximation of `t`. -/ rcases exists_countable_dense α with ⟨s, cs, s_dense⟩, - let v0 := {t : set α | finite t ∧ t ⊆ s}, + let v0 := {t : set α | t.finite ∧ t ⊆ s}, let v : set (nonempty_compacts α) := {t : nonempty_compacts α | (t : set α) ∈ v0}, refine ⟨⟨v, _, _⟩⟩, { have : countable v0, from countable_set_of_finite_subset cs, @@ -332,10 +332,10 @@ begin -- cover `t` with finitely many balls. Their centers form a set `a` have : totally_bounded (t : set α) := t.compact.totally_bounded, rcases totally_bounded_iff.1 this (δ/2) δpos' with ⟨a, af, ta⟩, - -- a : set α, af : finite a, ta : t ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2) + -- a : set α, af : a.finite, ta : t ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2) -- replace each center by a nearby approximation in `s`, giving a new set `b` let b := F '' a, - have : finite b := af.image _, + have : b.finite := af.image _, have tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ, { assume x hx, rcases mem_Union₂.1 (ta hx) with ⟨z, za, Dxz⟩, @@ -345,7 +345,7 @@ begin ... = δ : ennreal.add_halves _ }, -- keep only the points in `b` that are close to point in `t`, yielding a new set `c` let c := {y ∈ b | ∃ x ∈ t, edist x y < δ}, - have : finite c := ‹finite b›.subset (λx hx, hx.1), + have : c.finite := ‹b.finite›.subset (λx hx, hx.1), -- points in `t` are well approximated by points in `c` have tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ, { assume x hx, @@ -367,13 +367,13 @@ begin have hc : c.nonempty, from nonempty_of_Hausdorff_edist_ne_top t.nonempty (ne_top_of_lt Dtc), -- let `d` be the version of `c` in the type `nonempty_compacts α` - let d : nonempty_compacts α := ⟨⟨c, ‹finite c›.is_compact⟩, hc⟩, + let d : nonempty_compacts α := ⟨⟨c, ‹c.finite›.is_compact⟩, hc⟩, have : c ⊆ s, { assume x hx, rcases (mem_image _ _ _).1 hx.1 with ⟨y, ⟨ya, yx⟩⟩, rw ← yx, exact (Fspec y).1 }, - have : d ∈ v := ⟨‹finite c›, this⟩, + have : d ∈ v := ⟨‹c.finite›, this⟩, -- we have proved that `d` is a good approximation of `t` as requested exact ⟨d, ‹d ∈ v›, Dtc⟩ }, end, diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index cbd97c18a3a87..7b901a598e765 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/src/topology/metric_space/emetric_space.lean @@ -635,14 +635,14 @@ theorem cauchy_seq_iff_nnreal [nonempty β] [semilattice_sup β] {u : β → α} uniformity_basis_edist_nnreal.cauchy_seq_iff' theorem totally_bounded_iff {s : set α} : - totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε := + totally_bounded s ↔ ∀ ε > 0, ∃t : set α, t.finite ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, H _ (edist_mem_uniformity ε0), λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru, ⟨t, ft, h⟩ := H ε ε0 in ⟨t, ft, h.trans $ Union₂_mono $ λ y yt z, hε⟩⟩ theorem totally_bounded_iff' {s : set α} : - totally_bounded s ↔ ∀ ε > 0, ∃t⊆s, finite t ∧ s ⊆ ⋃y∈t, ball y ε := + totally_bounded s ↔ ∀ ε > 0, ∃t⊆s, set.finite t ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, (totally_bounded_iff_subset.1 H) _ (edist_mem_uniformity ε0), λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru, ⟨t, _, ft, h⟩ := H ε ε0 in diff --git a/src/topology/metric_space/gromov_hausdorff.lean b/src/topology/metric_space/gromov_hausdorff.lean index b55d1b10a459f..e08f4c8bc285d 100644 --- a/src/topology/metric_space/gromov_hausdorff.lean +++ b/src/topology/metric_space/gromov_hausdorff.lean @@ -593,12 +593,12 @@ begin refine second_countable_of_countable_discretization (λ δ δpos, _), let ε := (2/5) * δ, have εpos : 0 < ε := mul_pos (by norm_num) δpos, - have : ∀ p:GH_space, ∃ s : set p.rep, finite s ∧ (univ ⊆ (⋃x∈s, ball x ε)) := + have : ∀ p:GH_space, ∃ s : set p.rep, s.finite ∧ (univ ⊆ (⋃x∈s, ball x ε)) := λ p, by simpa using finite_cover_balls_of_compact (@compact_univ p.rep _ _) εpos, -- for each `p`, `s p` is a finite `ε`-dense subset of `p` (or rather the metric space -- `p.rep` representing `p`) choose s hs using this, - have : ∀ p:GH_space, ∀ t:set p.rep, finite t → ∃ n:ℕ, ∃ e:equiv t (fin n), true, + have : ∀ p:GH_space, ∀ t:set p.rep, t.finite → ∃ n:ℕ, ∃ e:equiv t (fin n), true, { assume p t ht, letI : fintype t := finite.fintype ht, exact ⟨fintype.card t, fintype.equiv_fin t, trivial⟩ }, diff --git a/src/topology/metric_space/hausdorff_dimension.lean b/src/topology/metric_space/hausdorff_dimension.lean index 59f7d7ff3dadf..a90ca84facfb1 100644 --- a/src/topology/metric_space/hausdorff_dimension.lean +++ b/src/topology/metric_space/hausdorff_dimension.lean @@ -194,7 +194,7 @@ bUnion_of_singleton s ▸ by simp only [dimH_bUnion hs, dimH_singleton, ennreal. alias dimH_countable ← set.countable.dimH_zero -lemma dimH_finite {s : set X} (hs : finite s) : dimH s = 0 := hs.countable.dimH_zero +lemma dimH_finite {s : set X} (hs : s.finite) : dimH s = 0 := hs.countable.dimH_zero alias dimH_finite ← set.finite.dimH_zero diff --git a/src/topology/metric_space/metric_separated.lean b/src/topology/metric_space/metric_separated.lean index 633a976644b6e..e487cb3325aca 100644 --- a/src/topology/metric_space/metric_separated.lean +++ b/src/topology/metric_space/metric_separated.lean @@ -80,7 +80,7 @@ lemma union_right {t'} (h : is_metric_separated s t) (h' : is_metric_separated s is_metric_separated s (t ∪ t') ↔ is_metric_separated s t ∧ is_metric_separated s t' := comm.trans $ union_left_iff.trans $ and_congr comm comm -lemma finite_Union_left_iff {ι : Type*} {I : set ι} (hI : finite I) {s : ι → set X} {t : set X} : +lemma finite_Union_left_iff {ι : Type*} {I : set ι} (hI : I.finite) {s : ι → set X} {t : set X} : is_metric_separated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, is_metric_separated (s i) t := begin refine finite.induction_on hI (by simp) (λ i I hi _ hI, _), @@ -89,7 +89,7 @@ end alias finite_Union_left_iff ↔ _ is_metric_separated.finite_Union_left -lemma finite_Union_right_iff {ι : Type*} {I : set ι} (hI : finite I) {s : set X} {t : ι → set X} : +lemma finite_Union_right_iff {ι : Type*} {I : set ι} (hI : I.finite) {s : set X} {t : ι → set X} : is_metric_separated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, is_metric_separated s (t i) := by simpa only [@comm _ _ s] using finite_Union_left_iff hI diff --git a/src/topology/metric_space/metrizable.lean b/src/topology/metric_space/metrizable.lean index e03629c52ded2..97b5512948e4c 100644 --- a/src/topology/metric_space/metrizable.lean +++ b/src/topology/metric_space/metrizable.lean @@ -193,7 +193,7 @@ begin `(U, V) ∈ T`. For `(U, V) ∉ T`, the same inequality is true because both `F y (U, V)` and `F x (U, V)` belong to the interval `[0, ε (U, V)]`. -/ refine (nhds_basis_closed_ball.comap _).ge_iff.2 (λ δ δ0, _), - have h_fin : finite {UV : s | δ ≤ ε UV}, by simpa only [← not_lt] using hε (gt_mem_nhds δ0), + have h_fin : {UV : s | δ ≤ ε UV}.finite, by simpa only [← not_lt] using hε (gt_mem_nhds δ0), have : ∀ᶠ y in 𝓝 x, ∀ UV, δ ≤ ε UV → dist (F y UV) (F x UV) ≤ δ, { refine (eventually_all_finite h_fin).2 (λ UV hUV, _), exact (f UV).continuous.tendsto x (closed_ball_mem_nhds _ δ0) }, diff --git a/src/topology/metric_space/shrinking_lemma.lean b/src/topology/metric_space/shrinking_lemma.lean index 71bbc4c21f794..4833ac1741977 100644 --- a/src/topology/metric_space/shrinking_lemma.lean +++ b/src/topology/metric_space/shrinking_lemma.lean @@ -31,7 +31,7 @@ so that each of the new balls has strictly smaller radius than the old one. This that `λ x, ball (c i) (r i)` is a locally finite covering and provides a covering indexed by the same type. -/ lemma exists_subset_Union_ball_radius_lt {r : ι → ℝ} (hs : is_closed s) - (uf : ∀ x ∈ s, finite {i | x ∈ ball (c i) (r i)}) (us : s ⊆ ⋃ i, ball (c i) (r i)) : + (uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.finite) (us : s ⊆ ⋃ i, ball (c i) (r i)) : ∃ r' : ι → ℝ, s ⊆ (⋃ i, ball (c i) (r' i)) ∧ ∀ i, r' i < r i := begin rcases exists_subset_Union_closed_subset hs (λ i, @is_open_ball _ _ (c i) (r i)) uf us @@ -44,7 +44,7 @@ end /-- Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one. -/ -lemma exists_Union_ball_eq_radius_lt {r : ι → ℝ} (uf : ∀ x, finite {i | x ∈ ball (c i) (r i)}) +lemma exists_Union_ball_eq_radius_lt {r : ι → ℝ} (uf : ∀ x, {i | x ∈ ball (c i) (r i)}.finite) (uU : (⋃ i, ball (c i) (r i)) = univ) : ∃ r' : ι → ℝ, (⋃ i, ball (c i) (r' i)) = univ ∧ ∀ i, r' i < r i := let ⟨r', hU, hv⟩ := exists_subset_Union_ball_radius_lt is_closed_univ (λ x _, uf x) uU.ge @@ -54,7 +54,7 @@ in ⟨r', univ_subset_iff.1 hU, hv⟩ of a closed subset of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one. -/ lemma exists_subset_Union_ball_radius_pos_lt {r : ι → ℝ} (hr : ∀ i, 0 < r i) (hs : is_closed s) - (uf : ∀ x ∈ s, finite {i | x ∈ ball (c i) (r i)}) (us : s ⊆ ⋃ i, ball (c i) (r i)) : + (uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.finite) (us : s ⊆ ⋃ i, ball (c i) (r i)) : ∃ r' : ι → ℝ, s ⊆ (⋃ i, ball (c i) (r' i)) ∧ ∀ i, r' i ∈ Ioo 0 (r i) := begin rcases exists_subset_Union_closed_subset hs (λ i, @is_open_ball _ _ (c i) (r i)) uf us @@ -68,7 +68,7 @@ end of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one. -/ lemma exists_Union_ball_eq_radius_pos_lt {r : ι → ℝ} (hr : ∀ i, 0 < r i) - (uf : ∀ x, finite {i | x ∈ ball (c i) (r i)}) (uU : (⋃ i, ball (c i) (r i)) = univ) : + (uf : ∀ x, {i | x ∈ ball (c i) (r i)}.finite) (uU : (⋃ i, ball (c i) (r i)) = univ) : ∃ r' : ι → ℝ, (⋃ i, ball (c i) (r' i)) = univ ∧ ∀ i, r' i ∈ Ioo 0 (r i) := let ⟨r', hU, hv⟩ := exists_subset_Union_ball_radius_pos_lt hr is_closed_univ (λ x _, uf x) uU.ge in ⟨r', univ_subset_iff.1 hU, hv⟩ diff --git a/src/topology/partition_of_unity.lean b/src/topology/partition_of_unity.lean index e84f667a35365..74706f16662cb 100644 --- a/src/topology/partition_of_unity.lean +++ b/src/topology/partition_of_unity.lean @@ -167,7 +167,7 @@ instance : has_coe_to_fun (bump_covering ι X s) (λ _, ι → C(X, ℝ)) := ⟨ protected lemma locally_finite : locally_finite (λ i, support (f i)) := f.locally_finite' -protected lemma point_finite (x : X) : finite {i | f i x ≠ 0} := +protected lemma point_finite (x : X) : {i | f i x ≠ 0}.finite := f.locally_finite.point_finite x lemma nonneg (i : ι) (x : X) : 0 ≤ f i x := f.nonneg' i x diff --git a/src/topology/separation.lean b/src/topology/separation.lean index dd698019bb8a4..0a12a7e03c342 100644 --- a/src/topology/separation.lean +++ b/src/topology/separation.lean @@ -584,7 +584,7 @@ end /-- Removing a finite set from a dense set in a space without isolated points, one still obtains a dense set. -/ lemma dense.diff_finite [t1_space α] [∀ (x : α), ne_bot (𝓝[≠] x)] - {s : set α} (hs : dense s) {t : set α} (ht : finite t) : + {s : set α} (hs : dense s) {t : set α} (ht : t.finite) : dense (s \ t) := begin convert hs.diff_finset ht.to_finset, diff --git a/src/topology/sequences.lean b/src/topology/sequences.lean index dfefa390e77e0..dd44dc78bf967 100644 --- a/src/topology/sequences.lean +++ b/src/topology/sequences.lean @@ -277,7 +277,7 @@ begin contrapose! h, rcases h with ⟨V, V_in, V_symm, h⟩, simp_rw [not_subset] at h, - have : ∀ (t : set β), finite t → ∃ a, a ∈ s ∧ a ∉ ⋃ y ∈ t, ball y V, + have : ∀ (t : set β), t.finite → ∃ a, a ∈ s ∧ a ∉ ⋃ y ∈ t, ball y V, { intros t ht, obtain ⟨a, a_in, H⟩ : ∃ a ∈ s, ∀ (x : β), x ∈ t → (x, a) ∉ V, by simpa [ht] using h t, diff --git a/src/topology/shrinking_lemma.lean b/src/topology/shrinking_lemma.lean index 31c7f0514b6d4..7c346e2dd8443 100644 --- a/src/topology/shrinking_lemma.lean +++ b/src/topology/shrinking_lemma.lean @@ -134,7 +134,7 @@ apply_eq_of_chain hc (find_mem _ _) hv /-- Least upper bound of a nonempty chain of partial refinements. -/ def chain_Sup (c : set (partial_refinement u s)) (hc : is_chain (≤) c) - (ne : c.nonempty) (hfin : ∀ x ∈ s, finite {i | x ∈ u i}) (hU : s ⊆ ⋃ i, u i) : + (ne : c.nonempty) (hfin : ∀ x ∈ s, {i | x ∈ u i}.finite) (hU : s ⊆ ⋃ i, u i) : partial_refinement u s := begin refine ⟨λ i, find c ne i i, chain_Sup_carrier c, @@ -160,7 +160,7 @@ end /-- `chain_Sup hu c hc ne hfin hU` is an upper bound of the chain `c`. -/ lemma le_chain_Sup {c : set (partial_refinement u s)} (hc : is_chain (≤) c) - (ne : c.nonempty) (hfin : ∀ x ∈ s, finite {i | x ∈ u i}) (hU : s ⊆ ⋃ i, u i) + (ne : c.nonempty) (hfin : ∀ x ∈ s, {i | x ∈ u i}.finite) (hU : s ⊆ ⋃ i, u i) {v} (hv : v ∈ c) : v ≤ chain_Sup c hc ne hfin hU := ⟨λ i hi, mem_bUnion hv hi, λ i hi, (find_apply_of_mem hc _ hv hi).symm⟩ @@ -207,7 +207,7 @@ variables {u : ι → set X} {s : set X} to a new open cover so that the closure of each new open set is contained in the corresponding original open set. -/ lemma exists_subset_Union_closure_subset (hs : is_closed s) (uo : ∀ i, is_open (u i)) - (uf : ∀ x ∈ s, finite {i | x ∈ u i}) (us : s ⊆ ⋃ i, u i) : + (uf : ∀ x ∈ s, {i | x ∈ u i}.finite) (us : s ⊆ ⋃ i, u i) : ∃ v : ι → set X, s ⊆ Union v ∧ (∀ i, is_open (v i)) ∧ ∀ i, closure (v i) ⊆ u i := begin classical, @@ -228,7 +228,7 @@ end to a new closed cover so that each new closed set is contained in the corresponding original open set. See also `exists_subset_Union_closure_subset` for a stronger statement. -/ lemma exists_subset_Union_closed_subset (hs : is_closed s) (uo : ∀ i, is_open (u i)) - (uf : ∀ x ∈ s, finite {i | x ∈ u i}) (us : s ⊆ ⋃ i, u i) : + (uf : ∀ x ∈ s, {i | x ∈ u i}.finite) (us : s ⊆ ⋃ i, u i) : ∃ v : ι → set X, s ⊆ Union v ∧ (∀ i, is_closed (v i)) ∧ ∀ i, v i ⊆ u i := let ⟨v, hsv, hvo, hv⟩ := exists_subset_Union_closure_subset hs uo uf us in ⟨λ i, closure (v i), subset.trans hsv (Union_mono $ λ i, subset_closure), @@ -237,7 +237,7 @@ in ⟨λ i, closure (v i), subset.trans hsv (Union_mono $ λ i, subset_closure), /-- Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new open cover so that the closure of each new open set is contained in the corresponding original open set. -/ -lemma exists_Union_eq_closure_subset (uo : ∀ i, is_open (u i)) (uf : ∀ x, finite {i | x ∈ u i}) +lemma exists_Union_eq_closure_subset (uo : ∀ i, is_open (u i)) (uf : ∀ x, {i | x ∈ u i}.finite) (uU : (⋃ i, u i) = univ) : ∃ v : ι → set X, Union v = univ ∧ (∀ i, is_open (v i)) ∧ ∀ i, closure (v i) ⊆ u i := let ⟨v, vU, hv⟩ := exists_subset_Union_closure_subset is_closed_univ uo (λ x _, uf x) uU.ge @@ -246,7 +246,7 @@ in ⟨v, univ_subset_iff.1 vU, hv⟩ /-- Shrinking lemma. A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new closed cover so that each of the new closed sets is contained in the corresponding original open set. See also `exists_Union_eq_closure_subset` for a stronger statement. -/ -lemma exists_Union_eq_closed_subset (uo : ∀ i, is_open (u i)) (uf : ∀ x, finite {i | x ∈ u i}) +lemma exists_Union_eq_closed_subset (uo : ∀ i, is_open (u i)) (uf : ∀ x, {i | x ∈ u i}.finite) (uU : (⋃ i, u i) = univ) : ∃ v : ι → set X, Union v = univ ∧ (∀ i, is_closed (v i)) ∧ ∀ i, v i ⊆ u i := let ⟨v, vU, hv⟩ := exists_subset_Union_closed_subset is_closed_univ uo (λ x _, uf x) uU.ge diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 76f053ddc7700..e248ad6b8f1cc 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -220,7 +220,7 @@ let ⟨t, ht⟩ := hs.elim_finite_subcover (λ i, (Z i)ᶜ) (λ i, (hZc i).is_op family of sets, then `f i ∩ s` is nonempty only for a finitely many `i`. -/ lemma locally_finite.finite_nonempty_inter_compact {ι : Type*} {f : ι → set α} (hf : locally_finite f) {s : set α} (hs : is_compact s) : - finite {i | (f i ∩ s).nonempty} := + {i | (f i ∩ s).nonempty}.finite := begin choose U hxU hUf using hf, rcases hs.elim_nhds_subcover U (λ x _, hxU x) with ⟨t, -, hsU⟩, @@ -283,7 +283,7 @@ is_compact.nonempty_Inter_of_directed_nonempty_compact_closed Z hZd hZn hZc hZcl /-- For every open cover of a compact set, there exists a finite subcover. -/ lemma is_compact.elim_finite_subcover_image {b : set ι} {c : ι → set α} (hs : is_compact s) (hc₁ : ∀ i ∈ b, is_open (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) : - ∃ b' ⊆ b, finite b' ∧ s ⊆ ⋃ i ∈ b', c i := + ∃ b' ⊆ b, set.finite b' ∧ s ⊆ ⋃ i ∈ b', c i := begin rcases hs.elim_finite_subcover (λ i, c i : b → set α) _ _ with ⟨d, hd⟩; [skip, simpa using hc₁, simpa using hc₂], @@ -387,7 +387,7 @@ lemma is_compact_singleton {a : α} : is_compact ({a} : set α) := lemma set.subsingleton.is_compact {s : set α} (hs : s.subsingleton) : is_compact s := subsingleton.induction_on hs is_compact_empty $ λ x, is_compact_singleton -lemma set.finite.compact_bUnion {s : set ι} {f : ι → set α} (hs : finite s) +lemma set.finite.compact_bUnion {s : set ι} {f : ι → set α} (hs : s.finite) (hf : ∀ i ∈ s, is_compact (f i)) : is_compact (⋃ i ∈ s, f i) := is_compact_of_finite_subcover $ assume ι U hUo hsU, @@ -417,7 +417,7 @@ lemma compact_Union {f : ι → set α} [fintype ι] (h : ∀ i, is_compact (f i)) : is_compact (⋃ i, f i) := by rw ← bUnion_univ; exact finite_univ.compact_bUnion (λ i _, h i) -lemma set.finite.is_compact (hs : finite s) : is_compact s := +lemma set.finite.is_compact (hs : s.finite) : is_compact s := bUnion_of_singleton s ▸ hs.compact_bUnion (λ _ _, is_compact_singleton) lemma is_compact.finite_of_discrete [discrete_topology α] {s : set α} (hs : is_compact s) : @@ -739,14 +739,14 @@ let ⟨t, ht⟩ := finite_cover_nhds_interior hU in ⟨t, univ_subset_iff.1 $ ht many nonempty elements. -/ lemma locally_finite.finite_nonempty_of_compact {ι : Type*} [compact_space α] {f : ι → set α} (hf : locally_finite f) : - finite {i | (f i).nonempty} := + {i | (f i).nonempty}.finite := by simpa only [inter_univ] using hf.finite_nonempty_inter_compact compact_univ /-- If `α` is a compact space, then a locally finite family of nonempty sets of `α` can have only finitely many elements, `set.finite` version. -/ lemma locally_finite.finite_of_compact {ι : Type*} [compact_space α] {f : ι → set α} (hf : locally_finite f) (hne : ∀ i, (f i).nonempty) : - finite (univ : set ι) := + (univ : set ι).finite := by simpa only [hne] using hf.finite_nonempty_of_compact /-- If `α` is a compact space, then a locally finite family of nonempty sets of `α` can have only diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean index 5d8a70689d356..ac31a3cdfac01 100644 --- a/src/topology/uniform_space/cauchy.lean +++ b/src/topology/uniform_space/cauchy.lean @@ -418,11 +418,11 @@ lemma is_closed.is_complete [complete_space α] {s : set α} /-- A set `s` is totally bounded if for every entourage `d` there is a finite set of points `t` such that every element of `s` is `d`-near to some element of `t`. -/ def totally_bounded (s : set α) : Prop := -∀d ∈ 𝓤 α, ∃t : set α, finite t ∧ s ⊆ (⋃ y ∈ t, {x | (x, y) ∈ d}) +∀d ∈ 𝓤 α, ∃t : set α, t.finite ∧ s ⊆ (⋃ y ∈ t, {x | (x, y) ∈ d}) theorem totally_bounded.exists_subset {s : set α} (hs : totally_bounded s) {U : set (α × α)} (hU : U ∈ 𝓤 α) : - ∃ t ⊆ s, finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U} := + ∃ t ⊆ s, set.finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U} := begin rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩, rcases hs r hr with ⟨k, fk, ks⟩, @@ -440,16 +440,16 @@ begin end theorem totally_bounded_iff_subset {s : set α} : totally_bounded s ↔ - ∀d ∈ 𝓤 α, ∃t ⊆ s, finite t ∧ s ⊆ (⋃y∈t, {x | (x,y) ∈ d}) := + ∀d ∈ 𝓤 α, ∃t ⊆ s, set.finite t ∧ s ⊆ (⋃y∈t, {x | (x,y) ∈ d}) := ⟨λ H d hd, H.exists_subset hd, λ H d hd, let ⟨t, _, ht⟩ := H d hd in ⟨t, ht⟩⟩ lemma filter.has_basis.totally_bounded_iff {ι} {p : ι → Prop} {U : ι → set (α × α)} (H : (𝓤 α).has_basis p U) {s : set α} : - totally_bounded s ↔ ∀ i, p i → ∃ t : set α, finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i} := + totally_bounded s ↔ ∀ i, p i → ∃ t : set α, set.finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i} := H.forall_iff $ λ U V hUV h, h.imp $ λ t ht, ⟨ht.1, ht.2.trans $ Union₂_mono $ λ x hx y hy, hUV hy⟩ lemma totally_bounded_of_forall_symm {s : set α} - (h : ∀ V ∈ 𝓤 α, symmetric_rel V → ∃ t : set α, finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) : + (h : ∀ V ∈ 𝓤 α, symmetric_rel V → ∃ t : set α, set.finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) : totally_bounded s := uniform_space.has_basis_symmetric.totally_bounded_iff.2 $ λ V hV, by simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2