diff --git a/src/topology/separation.lean b/src/topology/separation.lean index dd290846c87f9..55d1ab2591718 100644 --- a/src/topology/separation.lean +++ b/src/topology/separation.lean @@ -87,7 +87,7 @@ If the space is also compact: https://en.wikipedia.org/wiki/Separation_axiom -/ -open set filter +open set filter topological_space open_locale topological_space filter classical universes u v @@ -1051,6 +1051,17 @@ begin exact ⟨t, h2t, h3t, compact_closure_of_subset_compact hKc h1t⟩ end +/-- +In a locally compact T₂ space, every compact set has an open neighborhood with compact closure. +-/ +lemma exists_open_superset_and_is_compact_closure [locally_compact_space α] [t2_space α] + {K : set α} (hK : is_compact K) : ∃ V, is_open V ∧ K ⊆ V ∧ is_compact (closure V) := +begin + rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩, + refine ⟨interior K', is_open_interior, hKK', + compact_closure_of_subset_compact hK' interior_subset⟩, +end + lemma is_preirreducible_iff_subsingleton [t2_space α] (S : set α) : is_preirreducible S ↔ subsingleton S := begin @@ -1181,6 +1192,42 @@ begin tauto end +/-- +In a locally compact regular space, given a compact set `K` inside an open set `U`, we can find a +compact set `K'` between these sets: `K` is inside the interior of `K'` and `K' ⊆ U`. +-/ +lemma exists_compact_between [locally_compact_space α] [regular_space α] + {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) : + ∃ K', is_compact K' ∧ K ⊆ interior K' ∧ K' ⊆ U := +begin + choose C hxC hCU hC using λ x : K, nhds_is_closed (hU.mem_nhds $ hKU x.2), + choose L hL hxL using λ x : K, exists_compact_mem_nhds (x : α), + have : K ⊆ ⋃ x, interior (L x) ∩ interior (C x), from + λ x hx, mem_Union.mpr ⟨⟨x, hx⟩, + ⟨mem_interior_iff_mem_nhds.mpr (hxL _), mem_interior_iff_mem_nhds.mpr (hxC _)⟩⟩, + rcases hK.elim_finite_subcover _ _ this with ⟨t, ht⟩, + { refine ⟨⋃ x ∈ t, L x ∩ C x, t.compact_bUnion (λ x _, (hL x).inter_right (hC x)), λ x hx, _, _⟩, + { obtain ⟨y, hyt, hy : x ∈ interior (L y) ∩ interior (C y)⟩ := mem_bUnion_iff.mp (ht hx), + rw [← interior_inter] at hy, + refine interior_mono (subset_bUnion_of_mem hyt) hy }, + { simp_rw [Union_subset_iff], rintro x -, exact (inter_subset_right _ _).trans (hCU _) } }, + { exact λ _, is_open_interior.inter is_open_interior } +end + +/-- +In a locally compact regular space, given a compact set `K` inside an open set `U`, we can find a +open set `V` between these sets with compact closure: `K ⊆ V` and the closure of `V` is inside `U`. +-/ +lemma exists_open_between_and_is_compact_closure [locally_compact_space α] [regular_space α] + {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) : + ∃ V, is_open V ∧ K ⊆ V ∧ closure V ⊆ U ∧ is_compact (closure V) := +begin + rcases exists_compact_between hK hU hKU with ⟨V, hV, hKV, hVU⟩, + refine ⟨interior V, is_open_interior, hKV, + (closure_minimal interior_subset hV.is_closed).trans hVU, + compact_closure_of_subset_compact hV interior_subset⟩, +end + end regularity section normality @@ -1226,8 +1273,6 @@ begin exact compact_compact_separated hs.is_compact ht.is_compact st.eq_bot end -open topological_space - variable (α) /-- A regular topological space with second countable topology is a normal space. @@ -1352,8 +1397,6 @@ end section profinite -open topological_space - variables [t2_space α] /-- A Hausdorff space with a clopen basis is totally separated. -/ @@ -1443,8 +1486,6 @@ end profinite section locally_compact -open topological_space - variables {H : Type*} [topological_space H] [locally_compact_space H] [t2_space H] /-- A locally compact Hausdorff totally disconnected space has a basis with clopen elements. -/ diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 3ac3d9756b6c3..f3f56fdfa170f 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -50,14 +50,15 @@ open set filter classical topological_space open_locale classical topological_space filter universes u v -variables {α : Type u} {β : Type v} {ι : Type*} {π : ι → Type*} [topological_space α] {s t : set α} +variables {α : Type u} {β : Type v} {ι : Type*} {π : ι → Type*} +variables [topological_space α] [topological_space β] {s t : set α} /- compact sets -/ section compact /-- A set `s` is compact if for every nontrivial filter `f` that contains `s`, there exists `a ∈ s` such that every set of `f` meets every neighborhood of `a`. -/ -def is_compact (s : set α) := ∀ ⦃f⦄ [ne_bot f], f ≤ 𝓟 s → ∃a∈s, cluster_pt a f +def is_compact (s : set α) := ∀ ⦃f⦄ [ne_bot f], f ≤ 𝓟 s → ∃ a ∈ s, cluster_pt a f /-- The complement to a compact set belongs to a filter `f` if it belongs to each filter `𝓝 a ⊓ f`, `a ∈ s`. -/ @@ -125,7 +126,7 @@ lemma compact_of_is_closed_subset (hs : is_compact s) (ht : is_closed t) (h : t inter_eq_self_of_subset_right h ▸ hs.inter_right ht lemma is_compact.adherence_nhdset {f : filter α} - (hs : is_compact s) (hf₂ : f ≤ 𝓟 s) (ht₁ : is_open t) (ht₂ : ∀a∈s, cluster_pt a f → a ∈ t) : + (hs : is_compact s) (hf₂ : f ≤ 𝓟 s) (ht₁ : is_open t) (ht₂ : ∀ a ∈ s, cluster_pt a f → a ∈ t) : t ∈ f := classical.by_cases mem_of_eq_bot $ assume : f ⊓ 𝓟 tᶜ ≠ ⊥, @@ -141,7 +142,7 @@ classical.by_cases mem_of_eq_bot $ absurd A this lemma is_compact_iff_ultrafilter_le_nhds : - is_compact s ↔ (∀f : ultrafilter α, ↑f ≤ 𝓟 s → ∃a∈s, ↑f ≤ 𝓝 a) := + is_compact s ↔ (∀ f : ultrafilter α, ↑f ≤ 𝓟 s → ∃ a ∈ s, ↑f ≤ 𝓝 a) := begin refine (forall_ne_bot_le_iff _).trans _, { rintro f g hle ⟨a, has, haf⟩, @@ -154,7 +155,7 @@ alias is_compact_iff_ultrafilter_le_nhds ↔ is_compact.ultrafilter_le_nhds _ /-- For every open directed cover of a compact set, there exists a single element of the cover which itself includes the set. -/ lemma is_compact.elim_directed_cover {ι : Type v} [hι : nonempty ι] (hs : is_compact s) - (U : ι → set α) (hUo : ∀i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) (hdU : directed (⊆) U) : + (U : ι → set α) (hUo : ∀ i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) (hdU : directed (⊆) U) : ∃ i, s ⊆ U i := hι.elim $ λ i₀, is_compact.induction_on hs ⟨i₀, empty_subset _⟩ (λ s₁ s₂ hs ⟨i, hi⟩, ⟨i, subset.trans hs hi⟩) @@ -165,7 +166,7 @@ hι.elim $ λ i₀, is_compact.induction_on hs ⟨i₀, empty_subset _⟩ /-- For every open cover of a compact set, there exists a finite subcover. -/ lemma is_compact.elim_finite_subcover {ι : Type v} (hs : is_compact s) - (U : ι → set α) (hUo : ∀i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) : + (U : ι → set α) (hUo : ∀ i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t : finset ι, s ⊆ ⋃ i ∈ t, U i := hs.elim_directed_cover _ (λ t, is_open_bUnion $ λ i _, hUo i) (Union_eq_Union_finset U ▸ hsU) (directed_of_sup $ λ t₁ t₂ h, bUnion_subset_bUnion_left h) @@ -186,7 +187,7 @@ in ⟨t.image coe, λ x hx, let ⟨y, hyt, hyx⟩ := finset.mem_image.1 hx in hy /-- For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set. -/ lemma is_compact.elim_finite_subfamily_closed {s : set α} {ι : Type v} (hs : is_compact s) - (Z : ι → set α) (hZc : ∀i, is_closed (Z i)) (hsZ : s ∩ (⋂ i, Z i) = ∅) : + (Z : ι → set α) (hZc : ∀ i, is_closed (Z i)) (hsZ : s ∩ (⋂ i, Z i) = ∅) : ∃ t : finset ι, s ∩ (⋂ i ∈ t, Z i) = ∅ := let ⟨t, ht⟩ := hs.elim_finite_subcover (λ i, (Z i)ᶜ) (λ i, (hZc i).is_open_compl) (by simpa only [subset_def, not_forall, eq_empty_iff_forall_not_mem, mem_Union, @@ -212,7 +213,7 @@ end /-- To show that a compact set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every finite subfamily. -/ lemma is_compact.inter_Inter_nonempty {s : set α} {ι : Type v} (hs : is_compact s) - (Z : ι → set α) (hZc : ∀i, is_closed (Z i)) (hsZ : ∀ t : finset ι, (s ∩ ⋂ i ∈ t, Z i).nonempty) : + (Z : ι → set α) (hZc : ∀ i, is_closed (Z i)) (hsZ : ∀ t : finset ι, (s ∩ ⋂ i ∈ t, Z i).nonempty) : (s ∩ ⋂ i, Z i).nonempty := begin simp only [← ne_empty_iff_nonempty] at hsZ ⊢, @@ -261,9 +262,9 @@ have hZc : ∀ i, is_compact (Z i), from assume i, compact_of_is_closed_subset h 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 := +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 := begin rcases hs.elim_finite_subcover (λ i, c i : b → set α) _ _ with ⟨d, hd⟩; [skip, simpa using hc₁, simpa using hc₂], @@ -278,10 +279,10 @@ theorem is_compact_of_finite_subfamily_closed (h : Π {ι : Type u} (Z : ι → (set α)), (∀ i, is_closed (Z i)) → s ∩ (⋂ i, Z i) = ∅ → (∃ (t : finset ι), s ∩ (⋂ i ∈ t, Z i) = ∅)) : is_compact s := -assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, cluster_pt x f), - have hf : ∀x∈s, 𝓝 x ⊓ f = ⊥, +assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃ x ∈ s, cluster_pt x f), + have hf : ∀ x ∈ s, 𝓝 x ⊓ f = ⊥, by simpa only [cluster_pt, not_exists, not_not, ne_bot_iff], - have ¬ ∃x∈s, ∀t∈f.sets, x ∈ closure t, + have ¬ ∃ x ∈ s, ∀ t ∈ f.sets, x ∈ closure t, from assume ⟨x, hxs, hx⟩, have ∅ ∈ 𝓝 x ⊓ f, by rw [empty_mem_iff_bot, hf x hxs], let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := by rw [mem_inf_iff] at this; exact this in @@ -292,13 +293,13 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, cluster_pt by simp only [closure_eq_cluster_pts] at hx; exact (hx t₂ ht₂).ne this, 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, + have (⋂ i ∈ t, subtype.val i) ∈ f, from t.Inter_mem_sets.2 $ assume i hi, i.2, - have s ∩ (⋂i∈t, subtype.val i) ∈ f, + have s ∩ (⋂ i ∈ t, subtype.val i) ∈ f, from inter_mem (le_principal_iff.1 hfs) this, have ∅ ∈ f, from mem_of_superset this $ assume x ⟨hxs, hx⟩, - let ⟨i, hit, hxi⟩ := (show ∃i ∈ t, x ∉ closure (subtype.val i), + let ⟨i, hit, hxi⟩ := (show ∃ i ∈ t, x ∉ closure (subtype.val i), by { rw [eq_empty_iff_forall_not_mem] at ht, simpa [hxs, not_forall] using ht x }) in have x ∈ closure i.val, from subset_closure (mem_bInter_iff.mp hx i hit), show false, from hxi this, @@ -333,6 +334,27 @@ theorem is_compact_iff_finite_subfamily_closed : s ∩ (⋂ i, Z i) = ∅ → (∃ (t : finset ι), s ∩ (⋂ i ∈ t, Z i) = ∅)) := ⟨assume hs ι, hs.elim_finite_subfamily_closed, is_compact_of_finite_subfamily_closed⟩ +/-- +To show that `∀ y ∈ K, P x y` holds for `x` close enough to `x₀` when `K` is compact, +it is sufficient to show that for all `y₀ ∈ K` there `P x y` holds for `(x, y)` close enough +to `(x₀, y₀)`. +-/ +lemma is_compact.eventually_forall_of_forall_eventually {x₀ : α} {K : set β} (hK : is_compact K) + {P : α → β → Prop} (hP : ∀ y ∈ K, ∀ᶠ (z : α × β) in 𝓝 (x₀, y), P z.1 z.2): + ∀ᶠ x in 𝓝 x₀, ∀ y ∈ K, P x y := +begin + refine hK.induction_on _ _ _ _, + { exact eventually_of_forall (λ x y, false.elim) }, + { intros s t hst ht, refine ht.mono (λ x h y hys, h y $ hst hys) }, + { intros s t hs ht, filter_upwards [hs, ht], rintro x h1 h2 y (hys|hyt), + exacts [h1 y hys, h2 y hyt] }, + { intros y hyK, + specialize hP y hyK, + rw [nhds_prod_eq, eventually_prod_iff] at hP, + rcases hP with ⟨p, hp, q, hq, hpq⟩, + exact ⟨{y | q y}, mem_nhds_within_of_mem_nhds hq, eventually_of_mem hp @hpq⟩ } +end + @[simp] lemma is_compact_empty : is_compact (∅ : set α) := assume f hnf hsf, not.elim hnf.ne $ @@ -346,34 +368,34 @@ 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) - (hf : ∀i ∈ s, is_compact (f i)) : - is_compact (⋃i ∈ s, f i) := +lemma set.finite.compact_bUnion {s : set ι} {f : ι → set α} (hs : finite s) + (hf : ∀ i ∈ s, is_compact (f i)) : + is_compact (⋃ i ∈ s, f i) := is_compact_of_finite_subcover $ assume ι U hUo hsU, - have ∀i : subtype s, ∃t : finset ι, f i ⊆ (⋃ j ∈ t, U j), from + have ∀ i : subtype s, ∃ t : finset ι, f i ⊆ (⋃ j ∈ t, U j), from assume ⟨i, hi⟩, (hf i hi).elim_finite_subcover _ hUo - (calc f i ⊆ ⋃i ∈ s, f i : subset_bUnion_of_mem hi - ... ⊆ ⋃j, U j : hsU), + (calc f i ⊆ ⋃ i ∈ s, f i : subset_bUnion_of_mem hi + ... ⊆ ⋃ j, U j : hsU), let ⟨finite_subcovers, h⟩ := axiom_of_choice this in by haveI : fintype (subtype s) := hs.fintype; exact let t := finset.bUnion finset.univ finite_subcovers in - have (⋃i ∈ s, f i) ⊆ (⋃ i ∈ t, U i), from bUnion_subset $ + have (⋃ i ∈ s, f i) ⊆ (⋃ i ∈ t, U i), from bUnion_subset $ assume i hi, calc f i ⊆ (⋃ j ∈ finite_subcovers ⟨i, hi⟩, U j) : (h ⟨i, hi⟩) ... ⊆ (⋃ j ∈ t, U j) : bUnion_subset_bUnion_left $ assume j hj, finset.mem_bUnion.mpr ⟨_, finset.mem_univ _, hj⟩, ⟨t, this⟩ -lemma finset.compact_bUnion (s : finset β) {f : β → set α} (hf : ∀i ∈ s, is_compact (f i)) : - is_compact (⋃i ∈ s, f i) := +lemma finset.compact_bUnion (s : finset ι) {f : ι → set α} (hf : ∀ i ∈ s, is_compact (f i)) : + is_compact (⋃ i ∈ s, f i) := s.finite_to_set.compact_bUnion hf lemma compact_accumulate {K : ℕ → set α} (hK : ∀ n, is_compact (K n)) (n : ℕ) : is_compact (accumulate K n) := (finite_le_nat n).compact_bUnion $ λ k _, hK k -lemma compact_Union {f : β → set α} [fintype β] - (h : ∀i, is_compact (f i)) : is_compact (⋃i, f i) := +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 := @@ -478,8 +500,6 @@ end filter section tube_lemma -variables [topological_space β] - /-- `nhds_contain_boxes s t` means that any open neighborhood of `s × t` in `α × β` includes a product of an open neighborhood of `s` by an open neighborhood of `t`. -/ def nhds_contain_boxes (s : set α) (t : set β) : Prop := @@ -510,14 +530,14 @@ assume n hn hp, lemma nhds_contain_boxes_of_compact {s : set α} (hs : is_compact s) (t : set β) (H : ∀ x ∈ s, nhds_contain_boxes ({x} : set α) t) : nhds_contain_boxes s t := assume n hn hp, -have ∀x : s, ∃uv : set α × set β, +have ∀ x : s, ∃ uv : set α × set β, is_open uv.1 ∧ is_open uv.2 ∧ {↑x} ⊆ uv.1 ∧ t ⊆ uv.2 ∧ uv.1 ×ˢ uv.2 ⊆ n, from assume ⟨x, hx⟩, have ({x} : set α) ×ˢ t ⊆ n, from subset.trans (prod_mono (by simpa) subset.rfl) hp, let ⟨ux,vx,H1⟩ := H x hx n hn this in ⟨⟨ux,vx⟩,H1⟩, let ⟨uvs, h⟩ := classical.axiom_of_choice this in -have us_cover : s ⊆ ⋃i, (uvs i).1, from +have us_cover : s ⊆ ⋃ i, (uvs i).1, from assume x hx, subset_Union _ ⟨x,hx⟩ (by simpa using (h ⟨x,hx⟩).2.2.1), let ⟨s0, s0_cover⟩ := hs.elim_finite_subcover _ (λi, (h i).1) us_cover in @@ -527,7 +547,7 @@ have is_open u, from is_open_bUnion (λi _, (h i).1), have is_open v, from is_open_bInter s0.finite_to_set (λi _, (h i).2.1), have t ⊆ v, from subset_bInter (λi _, (h i).2.2.2.1), have u ×ˢ v ⊆ n, from assume ⟨x',y'⟩ ⟨hx',hy'⟩, - have ∃i ∈ s0, x' ∈ (uvs i).1, by simpa using hx', + have ∃ i ∈ s0, x' ∈ (uvs i).1, by simpa using hx', let ⟨i,is0,hi⟩ := this in (h i).2.2.2.2 ⟨hi, (bInter_subset_of_mem is0 : v ⊆ (uvs i).2) hy'⟩, ⟨u, v, ‹is_open u›, ‹is_open v›, s0_cover, ‹t ⊆ v›, ‹u ×ˢ v ⊆ n›⟩ @@ -561,7 +581,7 @@ lemma cluster_point_of_compact [compact_space α] (f : filter α) [ne_bot f] : ∃ x, cluster_pt x f := by simpa using compact_univ (show f ≤ 𝓟 univ, by simp) -lemma compact_space.elim_nhds_subcover {α : Type*} [topological_space α] [compact_space α] +lemma compact_space.elim_nhds_subcover [compact_space α] (U : α → set α) (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : finset α, (⋃ x ∈ t, U x) = ⊤ := begin @@ -569,7 +589,7 @@ begin exact ⟨t, by { rw eq_top_iff, exact s }⟩, end -theorem compact_space_of_finite_subfamily_closed {α : Type u} [topological_space α] +theorem compact_space_of_finite_subfamily_closed (h : Π {ι : Type u} (Z : ι → (set α)), (∀ i, is_closed (Z i)) → (⋂ i, Z i) = ∅ → ∃ (t : finset ι), (⋂ i ∈ t, Z i) = ∅) : compact_space α := @@ -650,8 +670,6 @@ noncomputable def locally_finite.fintype_of_compact {ι : Type*} [compact_space fintype ι := fintype_of_univ_finite (hf.finite_of_compact hne) -variables [topological_space β] - lemma is_compact.image_of_continuous_on {f : α → β} (hs : is_compact s) (hf : continuous_on f s) : is_compact (f '' s) := begin @@ -869,7 +887,7 @@ begin simp only [is_compact_iff_ultrafilter_le_nhds, nhds_pi, filter.pi, exists_prop, mem_set_of_eq, le_infi_iff, le_principal_iff], intros h f hfs, - have : ∀i:ι, ∃a, a∈s i ∧ tendsto (λx:Πi:ι, π i, x i) f (𝓝 a), + have : ∀ i:ι, ∃ a, a ∈ s i ∧ tendsto (λx:Πi:ι, π i, x i) f (𝓝 a), { refine λ i, h i (f.map _) (mem_map.2 _), exact mem_of_superset hfs (λ x hx, hx i) }, choose a ha, @@ -1255,7 +1273,7 @@ lemma is_clopen_Union {β : Type*} [fintype β] {s : β → set α} (h : ∀ i, is_clopen (s i)) : is_clopen (⋃ i, s i) := ⟨is_open_Union (forall_and_distrib.1 h).1, is_closed_Union (forall_and_distrib.1 h).2⟩ -lemma is_clopen_bUnion {β : Type*} {s : finset β} {f : β → set α} (h : ∀i ∈ s, is_clopen $ f i) : +lemma is_clopen_bUnion {β : Type*} {s : finset β} {f : β → set α} (h : ∀ i ∈ s, is_clopen $ f i) : is_clopen (⋃ i ∈ s, f i) := begin refine ⟨is_open_bUnion (λ i hi, (h i hi).1), _⟩, @@ -1268,13 +1286,13 @@ lemma is_clopen_Inter {β : Type*} [fintype β] {s : β → set α} (h : ∀ i, is_clopen (s i)) : is_clopen (⋂ i, s i) := ⟨(is_open_Inter (forall_and_distrib.1 h).1), (is_closed_Inter (forall_and_distrib.1 h).2)⟩ -lemma is_clopen_bInter {β : Type*} {s : finset β} {f : β → set α} (h : ∀i∈s, is_clopen (f i)) : - is_clopen (⋂i∈s, f i) := +lemma is_clopen_bInter {β : Type*} {s : finset β} {f : β → set α} (h : ∀ i ∈ s, is_clopen (f i)) : + is_clopen (⋂ i ∈ s, f i) := ⟨ is_open_bInter ⟨finset_coe.fintype s⟩ (λ i hi, (h i hi).1), by {show is_closed (⋂ (i : β) (H : i ∈ (↑s : set β)), f i), rw bInter_eq_Inter, apply is_closed_Inter, rintro ⟨i, hi⟩, exact (h i hi).2}⟩ -lemma continuous_on.preimage_clopen_of_clopen {β: Type*} [topological_space β] +lemma continuous_on.preimage_clopen_of_clopen {f : α → β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∩ f⁻¹' t) := ⟨continuous_on.preimage_open_of_open hf hs.1 ht.1, @@ -1300,7 +1318,7 @@ lemma clopen_range_sigma_mk {ι : Type*} {σ : ι → Type*} [Π i, topological_ is_clopen (set.range (@sigma.mk ι σ i)) := ⟨open_embedding_sigma_mk.open_range, closed_embedding_sigma_mk.closed_range⟩ -protected lemma quotient_map.is_clopen_preimage [topological_space β] {f : α → β} +protected lemma quotient_map.is_clopen_preimage {f : α → β} (hf : quotient_map f) {s : set β} : is_clopen (f ⁻¹' s) ↔ is_clopen s := and_congr hf.is_open_preimage hf.is_closed_preimage @@ -1421,7 +1439,7 @@ theorem nonempty_preirreducible_inter [preirreducible_space α] {s t : set α} : by simpa only [univ_inter, univ_subset_iff] using @preirreducible_space.is_preirreducible_univ α _ _ s t -theorem is_preirreducible.image [topological_space β] {s : set α} (H : is_preirreducible s) +theorem is_preirreducible.image {s : set α} (H : is_preirreducible s) (f : α → β) (hf : continuous_on f s) : is_preirreducible (f '' s) := begin rintros u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩, @@ -1440,7 +1458,7 @@ begin simp [*] } end -theorem is_irreducible.image [topological_space β] {s : set α} (H : is_irreducible s) +theorem is_irreducible.image {s : set α} (H : is_irreducible s) (f : α → β) (hf : continuous_on f s) : is_irreducible (f '' s) := ⟨nonempty_image_iff.mpr H.nonempty, H.is_preirreducible.image f hf⟩ @@ -1602,7 +1620,7 @@ lemma is_preirreducible.interior {Z : set α} (hZ : is_preirreducible Z) : is_preirreducible (interior Z) := hZ.open_subset is_open_interior interior_subset -lemma is_preirreducible.preimage [topological_space β] {Z : set α} (hZ : is_preirreducible Z) +lemma is_preirreducible.preimage {Z : set α} (hZ : is_preirreducible Z) {f : β → α} (hf : open_embedding f) : is_preirreducible (f ⁻¹' Z) := begin