From 279297937dede7b1b3451b7b0f1786352ad011fa Mon Sep 17 00:00:00 2001 From: sgouezel Date: Wed, 9 Nov 2022 09:39:41 +0000 Subject: [PATCH] chore(topology/*): rename compact_univ to is_compact_univ, and many more (#17436) Many lemma names about compact sets have `compact` instead of `is_compact` in their names, for historical reasons. We rename several of them to match more closely the naming convention. --- docs/overview.yaml | 4 +- docs/undergrad.yaml | 4 +- roadmap/topology/paracompact.lean | 2 +- .../morphisms/quasi_compact.lean | 5 +- .../morphisms/quasi_separated.lean | 4 +- src/algebraic_geometry/open_immersion.lean | 2 +- .../prime_spectrum/basic.lean | 2 +- src/analysis/convex/exposed.lean | 2 +- src/analysis/convex/krein_milman.lean | 5 +- src/analysis/convex/topology.lean | 6 +- src/analysis/convolution.lean | 4 +- src/analysis/normed_space/algebra.lean | 2 +- .../normed_space/compact_operator.lean | 6 +- .../normed_space/finite_dimension.lean | 2 +- src/analysis/normed_space/operator_norm.lean | 2 +- src/dynamics/omega_limit.lean | 8 +- src/geometry/manifold/bump_function.lean | 12 +-- src/geometry/manifold/partition_of_unity.lean | 2 +- .../constructions/borel_space.lean | 2 +- src/measure_theory/group/measure.lean | 3 +- src/measure_theory/measure/haar.lean | 2 +- src/measure_theory/measure/measure_space.lean | 2 +- src/topology/alexandroff.lean | 4 +- src/topology/algebra/group.lean | 2 +- src/topology/continuous_function/bounded.lean | 10 +-- .../continuous_function/cocompact_map.lean | 6 +- src/topology/continuous_function/compact.lean | 5 +- src/topology/discrete_quotient.lean | 2 +- src/topology/homeomorph.lean | 12 +-- src/topology/metric_space/antilipschitz.lean | 2 +- src/topology/metric_space/basic.lean | 16 ++-- src/topology/metric_space/closeds.lean | 9 ++- .../metric_space/gromov_hausdorff.lean | 6 +- .../gromov_hausdorff_realized.lean | 8 +- src/topology/noetherian_space.lean | 2 +- src/topology/paracompact.lean | 2 +- src/topology/separation.lean | 42 +++++----- src/topology/sequences.lean | 7 +- src/topology/sets/compacts.lean | 2 +- src/topology/spectral/hom.lean | 8 +- src/topology/stone_cech.lean | 2 +- src/topology/subset_properties.lean | 78 ++++++++++--------- src/topology/support.lean | 6 +- src/topology/uniform_space/cauchy.lean | 12 +-- src/topology/uniform_space/compact.lean | 2 +- .../uniform_space/compact_convergence.lean | 4 +- .../uniform_space/uniform_convergence.lean | 2 +- 47 files changed, 172 insertions(+), 162 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index c52c244e1f33a..b1eb32c9347a7 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -233,8 +233,8 @@ Topology: Metric spaces: metric space: 'metric_space' ball: 'metric.ball' - sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.compact_iff_seq_compact' - Heine-Borel theorem (proper metric space version): 'metric.compact_iff_closed_bounded' + sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.is_compact_iff_is_seq_compact' + Heine-Borel theorem (proper metric space version): 'metric.is_compact_iff_is_closed_bounded' Lipschitz continuity: 'lipschitz_with' Hölder continuity: 'holder_with' contraction mapping theorem: 'contracting_with.exists_fixed_point' diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml index 510b37c89d506..c219962bbf266 100644 --- a/docs/undergrad.yaml +++ b/docs/undergrad.yaml @@ -289,7 +289,7 @@ Single Variable Real Analysis: metric structure: 'real.metric_space' completeness of R: 'real.complete_space' Bolzano-Weierstrass theorem: 'tendsto_subseq_of_bounded' - compact subsets of $\R$: 'metric.compact_iff_closed_bounded' + compact subsets of $\R$: 'metric.is_compact_iff_is_closed_bounded' connected subsets of $\R$: 'set_of_is_preconnected_eq_of_ordered' additive subgroups of $\R$: 'real.subgroup_dense_or_cyclic' Numerical series: @@ -400,7 +400,7 @@ Topology: continuous functions: 'continuous' homeomorphisms: 'homeomorph' compactness in terms of open covers (Borel-Lebesgue): 'is_compact_iff_finite_subcover' - sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.compact_iff_seq_compact' + sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.is_compact_iff_is_seq_compact' connectedness: 'connected_space' connected components: 'connected_component' path connectedness: 'is_path_connected' diff --git a/roadmap/topology/paracompact.lean b/roadmap/topology/paracompact.lean index a5a4d718bb9ba..f0e05be5efbfd 100644 --- a/roadmap/topology/paracompact.lean +++ b/roadmap/topology/paracompact.lean @@ -55,7 +55,7 @@ lemma paracompact_of_compact {X : Type u} [topological_space X] [compact_space X begin refine ⟨λ α u uo uc, _⟩, obtain ⟨s, _, sf, sc⟩ := - compact_univ.elim_finite_subcover_image (λ a _, uo a) (by rwa [univ_subset_iff, bUnion_univ]), + is_compact_univ.elim_finite_subcover_image (λ a _, uo a) (by rwa [univ_subset_iff, bUnion_univ]), refine ⟨s, λ b, u b.val, λ b, uo b.val, _, _, λ b, ⟨b.val, subset.refl _⟩⟩, { todo }, { intro x, diff --git a/src/algebraic_geometry/morphisms/quasi_compact.lean b/src/algebraic_geometry/morphisms/quasi_compact.lean index 80e428e87aa7b..df052d7162205 100644 --- a/src/algebraic_geometry/morphisms/quasi_compact.lean +++ b/src/algebraic_geometry/morphisms/quasi_compact.lean @@ -94,7 +94,7 @@ begin intros H U hU hU', obtain ⟨S, hS, rfl⟩ := (is_compact_open_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩, simp only [set.preimage_Union, subtype.val_eq_coe], - exact hS.compact_bUnion (λ i _, H i i.prop) + exact hS.is_compact_bUnion (λ i _, H i i.prop) end @[simp] lemma quasi_compact.affine_property_to_property {X Y : Scheme} (f : X ⟶ Y) : @@ -167,7 +167,8 @@ begin rw ← hS, dsimp [opens.map], simp only [opens.coe_supr, set.preimage_Union, subtype.val_eq_coe], - exacts [compact_Union (λ i, is_compact_iff_compact_space.mpr (hS' i)), top_is_affine_open _] } + exacts [is_compact_Union (λ i, is_compact_iff_compact_space.mpr (hS' i)), + top_is_affine_open _] } end lemma quasi_compact.affine_open_cover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) : diff --git a/src/algebraic_geometry/morphisms/quasi_separated.lean b/src/algebraic_geometry/morphisms/quasi_separated.lean index 9d2309e4d81db..a28c5f20546d0 100644 --- a/src/algebraic_geometry/morphisms/quasi_separated.lean +++ b/src/algebraic_geometry/morphisms/quasi_separated.lean @@ -243,9 +243,9 @@ begin obtain ⟨s', hs', e'⟩ := (is_compact_open_iff_eq_basic_open_union _).mp ⟨hV', hV⟩, rw [e, e', set.Union₂_inter], simp_rw [set.inter_Union₂], - apply hs.compact_bUnion, + apply hs.is_compact_bUnion, { intros i hi, - apply hs'.compact_bUnion, + apply hs'.is_compact_bUnion, intros i' hi', change is_compact (X.basic_open i ⊓ X.basic_open i').1, rw ← Scheme.basic_open_mul, diff --git a/src/algebraic_geometry/open_immersion.lean b/src/algebraic_geometry/open_immersion.lean index 585a93f62396c..b140b1d5a85c3 100644 --- a/src/algebraic_geometry/open_immersion.lean +++ b/src/algebraic_geometry/open_immersion.lean @@ -1776,7 +1776,7 @@ lemma Scheme.open_cover.compact_space {X : Scheme} (𝒰 : X.open_cover) [finite begin casesI nonempty_fintype 𝒰.J, rw [← is_compact_univ_iff, ← 𝒰.Union_range], - apply compact_Union, + apply is_compact_Union, intro i, rw is_compact_iff_compact_space, exact @@homeomorph.compact_space _ _ (H i) diff --git a/src/algebraic_geometry/prime_spectrum/basic.lean b/src/algebraic_geometry/prime_spectrum/basic.lean index 2eea25e702772..91c4af98e6f72 100644 --- a/src/algebraic_geometry/prime_spectrum/basic.lean +++ b/src/algebraic_geometry/prime_spectrum/basic.lean @@ -787,7 +787,7 @@ end basic_open /-- The prime spectrum of a commutative ring is a compact topological space. -/ instance : compact_space (prime_spectrum R) := -{ compact_univ := by { convert is_compact_basic_open (1 : R), rw basic_open_one, refl } } +{ is_compact_univ := by { convert is_compact_basic_open (1 : R), rw basic_open_one, refl } } section order diff --git a/src/analysis/convex/exposed.lean b/src/analysis/convex/exposed.lean index 077073450dee8..ce6b1a7065137 100644 --- a/src/analysis/convex/exposed.lean +++ b/src/analysis/convex/exposed.lean @@ -199,7 +199,7 @@ end protected lemma is_compact [order_closed_topology 𝕜] [t2_space E] (hAB : is_exposed 𝕜 A B) (hA : is_compact A) : is_compact B := -compact_of_is_closed_subset hA (hAB.is_closed hA.is_closed) hAB.subset +is_compact_of_is_closed_subset hA (hAB.is_closed hA.is_closed) hAB.subset end is_exposed diff --git a/src/analysis/convex/krein_milman.lean b/src/analysis/convex/krein_milman.lean index f792106f221da..4619d869f6420 100644 --- a/src/analysis/convex/krein_milman.lean +++ b/src/analysis/convex/krein_milman.lean @@ -65,7 +65,7 @@ begin rwa ←eq_singleton_iff_unique_mem.2 ⟨hxt, λ y hyB, _⟩, by_contra hyx, obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx, - obtain ⟨z, hzt, hz⟩ := (compact_of_is_closed_subset hscomp htclos hst.1).exists_forall_ge + obtain ⟨z, hzt, hz⟩ := (is_compact_of_is_closed_subset hscomp htclos hst.1).exists_forall_ge ⟨x, hxt⟩ l.continuous.continuous_on, have h : is_exposed ℝ t {z ∈ t | ∀ w ∈ t, l w ≤ l z} := λ h, ⟨l, rfl⟩, rw ←hBmin {z ∈ t | ∀ w ∈ t, l w ≤ l z} ⟨⟨z, hzt, hz⟩, h.is_closed htclos, hst.trans @@ -79,7 +79,8 @@ begin haveI : nonempty ↥F := hFnemp.to_subtype, rw sInter_eq_Inter, refine is_compact.nonempty_Inter_of_directed_nonempty_compact_closed _ (λ t u, _) - (λ t, (hFS t.mem).1) (λ t, compact_of_is_closed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1) + (λ t, (hFS t.mem).1) + (λ t, is_compact_of_is_closed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1) (λ t, (hFS t.mem).2.1), obtain htu | hut := hF.total t.mem u.mem, exacts [⟨t, subset.rfl, htu⟩, ⟨u, hut, subset.rfl⟩], diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean index 33381ac9110e4..cb0e9dbc04058 100644 --- a/src/analysis/convex/topology.lean +++ b/src/analysis/convex/topology.lean @@ -72,8 +72,8 @@ lemma is_closed_std_simplex : is_closed (std_simplex ℝ ι) := (is_closed_eq (continuous_finset_sum _ $ λ x _, continuous_apply x) continuous_const) /-- `std_simplex ℝ ι` is compact. -/ -lemma compact_std_simplex : is_compact (std_simplex ℝ ι) := -metric.compact_iff_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩ +lemma is_compact_std_simplex : is_compact (std_simplex ℝ ι) := +metric.is_compact_iff_is_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩ end std_simplex @@ -216,7 +216,7 @@ lemma set.finite.compact_convex_hull {s : set E} (hs : s.finite) : is_compact (convex_hull ℝ s) := begin rw [hs.convex_hull_eq_image], - apply (compact_std_simplex _).image, + apply (is_compact_std_simplex _).image, haveI := hs.fintype, apply linear_map.continuous_on_pi end diff --git a/src/analysis/convolution.lean b/src/analysis/convolution.lean index 124a5916ebe51..a7eb92da24ff6 100644 --- a/src/analysis/convolution.lean +++ b/src/analysis/convolution.lean @@ -288,7 +288,7 @@ variables [topological_space G] [topological_add_group G] [borel_space G] lemma has_compact_support.convolution_exists_at {x₀ : G} (h : has_compact_support (λ t, L (f t) (g (x₀ - t)))) (hf : locally_integrable f μ) (hg : continuous g) : convolution_exists_at f g x₀ L μ := -((((homeomorph.neg G).trans $ homeomorph.add_right x₀).compact_preimage.mpr h).bdd_above_image +((((homeomorph.neg G).trans $ homeomorph.add_right x₀).is_compact_preimage.mpr h).bdd_above_image hg.norm.continuous_on).convolution_exists_at' L is_closed_closure.measurable_set subset_closure (hf h) hf.ae_strongly_measurable hg.ae_strongly_measurable @@ -485,7 +485,7 @@ variables [topological_add_group G] lemma has_compact_support.convolution [t2_space G] (hcf : has_compact_support f) (hcg : has_compact_support g) : has_compact_support (f ⋆[L, μ] g) := -compact_of_is_closed_subset (hcg.is_compact.add hcf) is_closed_closure $ closure_minimal +is_compact_of_is_closed_subset (hcg.is_compact.add hcf) is_closed_closure $ closure_minimal ((support_convolution_subset_swap L).trans $ add_subset_add subset_closure subset_closure) (hcg.is_compact.add hcf).is_closed diff --git a/src/analysis/normed_space/algebra.lean b/src/analysis/normed_space/algebra.lean index c935af4a5bcf7..d253557f7d743 100644 --- a/src/analysis/normed_space/algebra.lean +++ b/src/analysis/normed_space/algebra.lean @@ -47,7 +47,7 @@ begin { intros φ hφ, rw [set.mem_preimage, mem_closed_ball_zero_iff], exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ : _), }, - exact compact_of_is_closed_subset (is_compact_closed_ball 𝕜 0 _) character_space.is_closed h, + exact is_compact_of_is_closed_subset (is_compact_closed_ball 𝕜 0 _) character_space.is_closed h, end end character_space diff --git a/src/analysis/normed_space/compact_operator.lean b/src/analysis/normed_space/compact_operator.lean index 38ff69e6c926f..a643d74a688ce 100644 --- a/src/analysis/normed_space/compact_operator.lean +++ b/src/analysis/normed_space/compact_operator.lean @@ -87,7 +87,7 @@ lemma is_compact_operator_iff_exists_mem_nhds_is_compact_closure_image [t2_space is_compact_operator f ↔ ∃ V ∈ (𝓝 0 : filter M₁), is_compact (closure $ f '' V) := begin rw is_compact_operator_iff_exists_mem_nhds_image_subset_compact, - exact ⟨λ ⟨V, hV, K, hK, hKV⟩, ⟨V, hV, compact_closure_of_subset_compact hK hKV⟩, + exact ⟨λ ⟨V, hV, K, hK, hKV⟩, ⟨V, hV, is_compact_closure_of_subset_compact hK hKV⟩, λ ⟨V, hV, hVc⟩, ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩, end @@ -113,7 +113,7 @@ lemma is_compact_operator.is_compact_closure_image_of_vonN_bounded [t2_space M {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : is_compact_operator f) {S : set M₁} (hS : is_vonN_bounded 𝕜₁ S) : is_compact (closure $ f '' S) := let ⟨K, hK, hKf⟩ := hf.image_subset_compact_of_vonN_bounded hS in -compact_closure_of_subset_compact hK hKf +is_compact_closure_of_subset_compact hK hKf end bounded @@ -388,7 +388,7 @@ begin { change is_compact_operator (u : M₁ →ₛₗ[σ₁₂] M₂), rw is_compact_operator_iff_is_compact_closure_image_closed_ball (u : M₁ →ₛₗ[σ₁₂] M₂) zero_lt_one, - exact compact_of_totally_bounded_is_closed this.closure is_closed_closure }, + exact is_compact_of_totally_bounded_is_closed this.closure is_closed_closure }, rw metric.totally_bounded_iff, intros ε hε, rcases hu (ε/2) (by linarith) with ⟨v, hv, huv⟩, diff --git a/src/analysis/normed_space/finite_dimension.lean b/src/analysis/normed_space/finite_dimension.lean index 26a743b54627a..ff577641df3a9 100644 --- a/src/analysis/normed_space/finite_dimension.lean +++ b/src/analysis/normed_space/finite_dimension.lean @@ -644,7 +644,7 @@ begin rcases hx' with ⟨r, hr₀, hrK⟩, haveI : finite_dimensional ℝ E, from finite_dimensional_of_is_compact_closed_ball ℝ hr₀ - (compact_of_is_closed_subset hK metric.is_closed_ball hrK), + (is_compact_of_is_closed_subset hK metric.is_closed_ball hrK), exact exists_mem_frontier_inf_dist_compl_eq_dist hx hK.ne_univ }, { refine ⟨x, hx', _⟩, rw frontier_eq_closure_inter_closure at hx', diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean index 20e53e52c177f..ee029f60564f7 100644 --- a/src/analysis/normed_space/operator_norm.lean +++ b/src/analysis/normed_space/operator_norm.lean @@ -1538,7 +1538,7 @@ lemma is_compact_closure_image_coe_of_bounded [proper_space F] {s : set (E' →S is_compact (closure ((coe_fn : (E' →SL[σ₁₂] F) → E' → F) '' s)) := have ∀ x, is_compact (closure (apply' F σ₁₂ x '' s)), from λ x, ((apply' F σ₁₂ x).lipschitz.bounded_image hb).is_compact_closure, -compact_closure_of_subset_compact (is_compact_pi_infinite this) +is_compact_closure_of_subset_compact (is_compact_pi_infinite this) (image_subset_iff.2 $ λ g hg x, subset_closure $ mem_image_of_mem _ hg) /-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values diff --git a/src/dynamics/omega_limit.lean b/src/dynamics/omega_limit.lean index ccdbced232442..0e95a6320dcb6 100644 --- a/src/dynamics/omega_limit.lean +++ b/src/dynamics/omega_limit.lean @@ -218,7 +218,7 @@ begin rcases hc₂ with ⟨v, hv₁, hv₂⟩, let k := closure (image2 ϕ v s), have hk : is_compact (k \ n) := - is_compact.diff (compact_of_is_closed_subset hc₁ is_closed_closure hv₂) hn₁, + is_compact.diff (is_compact_of_is_closed_subset hc₁ is_closed_closure hv₂) hn₁, let j := λ u, (closure (image2 ϕ (u ∩ v) s))ᶜ, have hj₁ : ∀ u ∈ f, is_open (j u), from λ _ _, (is_open_compl_iff.mpr is_closed_closure), @@ -279,7 +279,7 @@ lemma eventually_closure_subset_of_is_open_of_omega_limit_subset [compact_space {v : set β} (hv₁ : is_open v) (hv₂ : ω f ϕ s ⊆ v) : ∃ u ∈ f, closure (image2 ϕ u s) ⊆ v := eventually_closure_subset_of_is_compact_absorbing_of_is_open_of_omega_limit_subset' - _ _ _ compact_univ ⟨univ, univ_mem, subset_univ _⟩ hv₁ hv₂ + _ _ _ is_compact_univ ⟨univ, univ_mem, subset_univ _⟩ hv₁ hv₂ lemma eventually_maps_to_of_is_open_of_omega_limit_subset [compact_space β] {v : set β} (hv₁ : is_open v) (hv₂ : ω f ϕ s ⊆ v) : @@ -308,7 +308,7 @@ begin nonempty.image2 (nonempty_of_mem (inter_mem u.prop hv₁)) hs, exact hn.mono subset_closure }, { intro _, - apply compact_of_is_closed_subset hc₁ is_closed_closure, + apply is_compact_of_is_closed_subset hc₁ is_closed_closure, calc _ ⊆ closure (image2 ϕ v s) : closure_mono (image2_subset (inter_subset_right _ _) subset.rfl) ... ⊆ c : hv₂ }, @@ -318,7 +318,7 @@ end lemma nonempty_omega_limit [compact_space β] [ne_bot f] (hs : s.nonempty) : (ω f ϕ s).nonempty := nonempty_omega_limit_of_is_compact_absorbing _ _ _ - compact_univ ⟨univ, univ_mem, subset_univ _⟩ hs + is_compact_univ ⟨univ, univ_mem, subset_univ _⟩ hs end omega_limit diff --git a/src/geometry/manifold/bump_function.lean b/src/geometry/manifold/bump_function.lean index a9e8b916682db..9dfc004e3c77e 100644 --- a/src/geometry/manifold/bump_function.lean +++ b/src/geometry/manifold/bump_function.lean @@ -104,7 +104,7 @@ by rw [coe_def, support_indicator, (∘), support_comp_eq_preimage, ← ext_char ← (ext_chart_at I c).symm_image_target_inter_eq', ← (ext_chart_at I c).symm_image_target_inter_eq', f.to_cont_diff_bump.support_eq] -lemma open_support : is_open (support f) := +lemma is_open_support : is_open (support f) := by { rw support_eq_inter_preimage, exact ext_chart_preimage_open_of_open I c is_open_ball } lemma support_eq_symm_image : @@ -193,7 +193,7 @@ begin self_mem_nhds_within } end -lemma closed_image_of_closed {s : set M} (hsc : is_closed s) (hs : s ⊆ support f) : +lemma is_closed_image_of_is_closed {s : set M} (hsc : is_closed s) (hs : s ⊆ support f) : is_closed (ext_chart_at I c '' s) := begin rw f.image_eq_inter_preimage_of_subset_support hs, @@ -210,7 +210,7 @@ lemma exists_r_pos_lt_subset_ball {s : set M} (hsc : is_closed s) (hs : s ⊆ su (chart_at H c).source ∩ ext_chart_at I c ⁻¹' (ball (ext_chart_at I c c) r) := begin set e := ext_chart_at I c, - have : is_closed (e '' s) := f.closed_image_of_closed hsc hs, + have : is_closed (e '' s) := f.is_closed_image_of_is_closed hsc hs, rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs, rcases euclidean.exists_pos_lt_subset_ball f.R_pos this hs.2 with ⟨r, hrR, hr⟩, exact ⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩ @@ -233,7 +233,7 @@ classical.inhabited_of_nonempty nhds_within_range_basis.nonempty variables [t2_space M] -lemma closed_symm_image_closed_ball : +lemma is_closed_symm_image_closed_ball : is_closed ((ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)) := f.compact_symm_image_closed_ball.is_closed @@ -242,7 +242,7 @@ lemma tsupport_subset_symm_image_closed_ball : begin rw [tsupport, support_eq_symm_image], exact closure_minimal (image_subset _ $ inter_subset_inter_left _ ball_subset_closed_ball) - f.closed_symm_image_closed_ball + f.is_closed_symm_image_closed_ball end lemma tsupport_subset_ext_chart_at_source : @@ -260,7 +260,7 @@ lemma tsupport_subset_chart_at_source : by simpa only [ext_chart_at_source] using f.tsupport_subset_ext_chart_at_source protected lemma has_compact_support : has_compact_support f := -compact_of_is_closed_subset f.compact_symm_image_closed_ball is_closed_closure +is_compact_of_is_closed_subset f.compact_symm_image_closed_ball is_closed_closure f.tsupport_subset_symm_image_closed_ball variables (I c) diff --git a/src/geometry/manifold/partition_of_unity.lean b/src/geometry/manifold/partition_of_unity.lean index ba080f814e3e4..64cd831e553e0 100644 --- a/src/geometry/manifold/partition_of_unity.lean +++ b/src/geometry/manifold/partition_of_unity.lean @@ -297,7 +297,7 @@ begin rcases refinement_of_locally_compact_sigma_compact_of_nhds_basis_set hs hB with ⟨ι, c, f, hf, hsub', hfin⟩, choose hcs hfU using hf, /- Then we use the shrinking lemma to get a covering by smaller open -/ - rcases exists_subset_Union_closed_subset hs (λ i, (f i).open_support) + rcases exists_subset_Union_closed_subset hs (λ i, (f i).is_open_support) (λ x hx, hfin.point_finite x) hsub' with ⟨V, hsV, hVc, hVf⟩, choose r hrR hr using λ i, (f i).exists_r_pos_lt_subset_ball (hVc i) (hVf i), refine ⟨ι, ⟨c, λ i, (f i).update_r (r i) (hrR i), hcs, _, λ x hx, _⟩, λ i, _⟩, diff --git a/src/measure_theory/constructions/borel_space.lean b/src/measure_theory/constructions/borel_space.lean index 341d5e46b0317..efd773d8f5694 100644 --- a/src/measure_theory/constructions/borel_space.lean +++ b/src/measure_theory/constructions/borel_space.lean @@ -1309,7 +1309,7 @@ protected lemma is_finite_measure_on_compacts.map assume K hK, rw [measure.map_apply f.measurable hK.measurable_set], apply is_compact.measure_lt_top, - rwa f.compact_preimage + rwa f.is_compact_preimage end⟩ end borel_space diff --git a/src/measure_theory/group/measure.lean b/src/measure_theory/group/measure.lean index 509b41461d233..20485954aa704 100644 --- a/src/measure_theory/group/measure.lean +++ b/src/measure_theory/group/measure.lean @@ -537,7 +537,8 @@ lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [gro lt_top_of_is_compact := begin assume K hK, rw map_apply hf.measurable hK.measurable_set, - exact is_compact.measure_lt_top ((⟨⟨f, hf⟩, h_prop⟩ : cocompact_map G H).compact_preimage hK), + exact is_compact.measure_lt_top + ((⟨⟨f, hf⟩, h_prop⟩ : cocompact_map G H).is_compact_preimage hK), end, to_is_open_pos_measure := hf.is_open_pos_measure_map h_surj } diff --git a/src/measure_theory/measure/haar.lean b/src/measure_theory/measure/haar.lean index e08452da3378c..011bb8d2ee72b 100644 --- a/src/measure_theory/measure/haar.lean +++ b/src/measure_theory/measure/haar.lean @@ -419,7 +419,7 @@ end lemma chaar_sup_eq [t2_space G] {K₀ : positive_compacts G} {K₁ K₂ : compacts G} (h : disjoint K₁.1 K₂.1) : chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂ := begin - rcases compact_compact_separated K₁.2 K₂.2 h with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩, + rcases is_compact_is_compact_separated K₁.2 K₂.2 h with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩, rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩, rcases mem_nhds_iff.mp h1L₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩, replace h2L₁ := subset.trans (mul_subset_mul_left h1V₁) h2L₁, diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 8838e691cc3d6..e9bd8b37b57e0 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -3217,7 +3217,7 @@ protected lemma is_finite_measure_on_compacts.smul [topological_space α] (μ : lemma compact_space.is_finite_measure [topological_space α] [compact_space α] [is_finite_measure_on_compacts μ] : is_finite_measure μ := -⟨is_finite_measure_on_compacts.lt_top_of_is_compact compact_univ⟩ +⟨is_finite_measure_on_compacts.lt_top_of_is_compact is_compact_univ⟩ omit m0 diff --git a/src/topology/alexandroff.lean b/src/topology/alexandroff.lean index 581c82ff0c0a1..fe906be994646 100644 --- a/src/topology/alexandroff.lean +++ b/src/topology/alexandroff.lean @@ -149,7 +149,7 @@ instance : topological_space (alexandroff X) := suffices : is_open (coe ⁻¹' ⋃₀ S : set X), { refine ⟨_, this⟩, rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩, - refine compact_of_is_closed_subset ((ho s hsS).1 hs) this.is_closed_compl _, + refine is_compact_of_is_closed_subset ((ho s hsS).1 hs) this.is_closed_compl _, exact compl_subset_compl.mpr (preimage_mono $ subset_sUnion_of_mem hsS) }, rw [preimage_sUnion], exact is_open_bUnion (λ s hs, (ho s hs).2) @@ -356,7 +356,7 @@ Finally, if the original space `X` is *not* compact and is a preconnected space, /-- For any topological space `X`, its one point compactification is a compact space. -/ instance : compact_space (alexandroff X) := -{ compact_univ := +{ is_compact_univ := begin have : tendsto (coe : X → alexandroff X) (cocompact X) (𝓝 ∞), { rw [nhds_infty_eq], diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean index 9973f72f41125..9d5d9fbf0b8ec 100644 --- a/src/topology/algebra/group.lean +++ b/src/topology/algebra/group.lean @@ -1180,7 +1180,7 @@ instance separable_locally_compact_group.sigma_compact_space begin obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G), refine ⟨⟨λ n, (λ x, x * dense_seq G n) ⁻¹' L, _, _⟩⟩, - { intro n, exact (homeomorph.mul_right _).compact_preimage.mpr hLc }, + { intro n, exact (homeomorph.mul_right _).is_compact_preimage.mpr hLc }, { refine Union_eq_univ_iff.2 (λ x, _), obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (range (dense_seq G) ∩ (λ y, x * y) ⁻¹' L).nonempty, { rw [← (homeomorph.mul_left x).apply_symm_apply 1] at hL1, diff --git a/src/topology/continuous_function/bounded.lean b/src/topology/continuous_function/bounded.lean index 82e54545a794e..33dfeb15c4493 100644 --- a/src/topology/continuous_function/bounded.lean +++ b/src/topology/continuous_function/bounded.lean @@ -152,7 +152,7 @@ lemma dist_lt_of_nonempty_compact [nonempty α] [compact_space α] begin have c : continuous (λ x, dist (f x) (g x)), { continuity, }, obtain ⟨x, -, le⟩ := - is_compact.exists_forall_ge compact_univ set.univ_nonempty (continuous.continuous_on c), + is_compact.exists_forall_ge is_compact_univ set.univ_nonempty (continuous.continuous_on c), exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr (λ y, le y trivial)) (w x), end @@ -421,7 +421,7 @@ theorem arzela_ascoli₁ [compact_space β] f ∈ A → dist (f y) (f z) < ε) : is_compact A := begin - refine compact_of_totally_bounded_is_closed _ closed, + refine is_compact_of_totally_bounded_is_closed _ closed, refine totally_bounded_of_finite_discretization (λ ε ε0, _), rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩, let ε₂ := ε₁/2/2, @@ -442,11 +442,11 @@ begin /- For all x, the set hU x is an open set containing x on which the elements of A fluctuate by at most ε₂. We extract finitely many of these sets that cover the whole space, by compactness -/ - rcases compact_univ.elim_finite_subcover_image + rcases is_compact_univ.elim_finite_subcover_image (λx _, (hU x).2.1) (λx hx, mem_bUnion (mem_univ _) (hU x).1) with ⟨tα, _, ⟨_⟩, htα⟩, /- tα : set α, htα : univ ⊆ ⋃x ∈ tα, U x -/ - rcases @finite_cover_balls_of_compact β _ _ compact_univ _ ε₂0 + rcases @finite_cover_balls_of_compact β _ _ is_compact_univ _ ε₂0 with ⟨tβ, _, ⟨_⟩, htβ⟩, resetI, /- tβ : set β, htβ : univ ⊆ ⋃y ∈ tβ, ball y ε₂ -/ /- Associate to every point `y` in the space a nearby point `F y` in tβ -/ @@ -489,7 +489,7 @@ using compactness there and then lifting everything to the original space. -/ begin have M : lipschitz_with 1 coe := lipschitz_with.subtype_coe s, let F : (α →ᵇ s) → α →ᵇ β := comp coe M, - refine compact_of_is_closed_subset + refine is_compact_of_is_closed_subset ((_ : is_compact (F ⁻¹' A)).image (continuous_comp M)) closed (λ f hf, _), { haveI : compact_space s := is_compact_iff_compact_space.1 hs, refine arzela_ascoli₁ _ (continuous_iff_is_closed.1 (continuous_comp M) _ closed) diff --git a/src/topology/continuous_function/cocompact_map.lean b/src/topology/continuous_function/cocompact_map.lean index 38dead31b9d55..b0532fb87d55d 100644 --- a/src/topology/continuous_function/cocompact_map.lean +++ b/src/topology/continuous_function/cocompact_map.lean @@ -22,7 +22,7 @@ open filter set tends to the cocompact filter along the cocompact filter. Functions for which preimages of compact sets are compact always satisfy this property, and the converse holds for cocompact continuous maps when the codomain is Hausdorff (see `cocompact_map.tendsto_of_forall_preimage` and -`cocompact_map.compact_preimage`). +`cocompact_map.is_compact_preimage`). Cocompact maps thus generalise proper maps, with which they correspond when the codomain is Hausdorff. -/ @@ -119,13 +119,13 @@ lemma tendsto_of_forall_preimage {f : α → β} (h : ∀ s, is_compact s → is /-- If the codomain is Hausdorff, preimages of compact sets are compact under a cocompact continuous map. -/ -lemma compact_preimage [t2_space β] (f : cocompact_map α β) ⦃s : set β⦄ (hs : is_compact s) : +lemma is_compact_preimage [t2_space β] (f : cocompact_map α β) ⦃s : set β⦄ (hs : is_compact s) : is_compact (f ⁻¹' s) := begin obtain ⟨t, ht, hts⟩ := mem_cocompact'.mp (by simpa only [preimage_image_preimage, preimage_compl] using mem_map.mp (cocompact_tendsto f $ mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩)), - exact compact_of_is_closed_subset ht (hs.is_closed.preimage $ map_continuous f) + exact is_compact_of_is_closed_subset ht (hs.is_closed.preimage $ map_continuous f) (by simpa using hts), end diff --git a/src/topology/continuous_function/compact.lean b/src/topology/continuous_function/compact.lean index 00929bfc10e36..d113fe1c3e47d 100644 --- a/src/topology/continuous_function/compact.lean +++ b/src/topology/continuous_function/compact.lean @@ -55,8 +55,9 @@ begin simp only [has_basis_compact_convergence_uniformity.mem_iff, uniformity_basis_dist_le.mem_iff], exact λ s, ⟨λ ⟨⟨a, b⟩, ⟨ha, ⟨ε, hε, hb⟩⟩, hs⟩, ⟨{p | ∀ x, (p.1 x, p.2 x) ∈ b}, ⟨ε, hε, λ _ h x, hb (by exact (dist_le hε.le).mp h x)⟩, λ f g h, hs (by exact λ x hx, h x)⟩, - λ ⟨t, ⟨ε, hε, ht⟩, hs⟩, ⟨⟨set.univ, {p | dist p.1 p.2 ≤ ε}⟩, ⟨compact_univ, ⟨ε, hε, λ _ h, h⟩⟩, - λ ⟨f, g⟩ h, hs _ _ (ht (by exact (dist_le hε.le).mpr (λ x, h x (mem_univ x))))⟩⟩, + λ ⟨t, ⟨ε, hε, ht⟩, hs⟩, ⟨⟨set.univ, {p | dist p.1 p.2 ≤ ε}⟩, + ⟨is_compact_univ, ⟨ε, hε, λ _ h, h⟩⟩, + λ ⟨f, g⟩ h, hs _ _ (ht (by exact (dist_le hε.le).mpr (λ x, h x (mem_univ x))))⟩⟩, end lemma uniform_embedding_equiv_bounded_of_compact : diff --git a/src/topology/discrete_quotient.lean b/src/topology/discrete_quotient.lean index bded7b0c1086e..16cc4543bb6fd 100644 --- a/src/topology/discrete_quotient.lean +++ b/src/topology/discrete_quotient.lean @@ -326,7 +326,7 @@ end noncomputable instance [compact_space X] : fintype S := begin - have cond : is_compact (⊤ : set X) := compact_univ, + have cond : is_compact (⊤ : set X) := is_compact_univ, rw is_compact_iff_finite_subcover at cond, have h := @cond S (λ s, S.proj ⁻¹' {s}) (λ s, fiber_open _ _) (λ x hx, ⟨S.proj ⁻¹' {S.proj x}, ⟨S.proj x, rfl⟩, rfl⟩), diff --git a/src/topology/homeomorph.lean b/src/topology/homeomorph.lean index 06860a720f17f..edadf75d322b0 100644 --- a/src/topology/homeomorph.lean +++ b/src/topology/homeomorph.lean @@ -175,23 +175,23 @@ protected lemma second_countable_topology [topological_space.second_countable_to topological_space.second_countable_topology α := h.inducing.second_countable_topology -lemma compact_image {s : set α} (h : α ≃ₜ β) : is_compact (h '' s) ↔ is_compact s := +lemma is_compact_image {s : set α} (h : α ≃ₜ β) : is_compact (h '' s) ↔ is_compact s := h.embedding.is_compact_iff_is_compact_image.symm -lemma compact_preimage {s : set β} (h : α ≃ₜ β) : is_compact (h ⁻¹' s) ↔ is_compact s := -by rw ← image_symm; exact h.symm.compact_image +lemma is_compact_preimage {s : set β} (h : α ≃ₜ β) : is_compact (h ⁻¹' s) ↔ is_compact s := +by rw ← image_symm; exact h.symm.is_compact_image @[simp] lemma comap_cocompact (h : α ≃ₜ β) : comap h (cocompact β) = cocompact α := (comap_cocompact_le h.continuous).antisymm $ (has_basis_cocompact.le_basis_iff (has_basis_cocompact.comap h)).2 $ λ K hK, - ⟨h ⁻¹' K, h.compact_preimage.2 hK, subset.rfl⟩ + ⟨h ⁻¹' K, h.is_compact_preimage.2 hK, subset.rfl⟩ @[simp] lemma map_cocompact (h : α ≃ₜ β) : map h (cocompact α) = cocompact β := by rw [← h.comap_cocompact, map_comap_of_surjective h.surjective] protected lemma compact_space [compact_space α] (h : α ≃ₜ β) : compact_space β := -{ compact_univ := by { rw [← image_univ_of_surjective h.surjective, h.compact_image], - apply compact_space.compact_univ } } +{ is_compact_univ := by { rw [← image_univ_of_surjective h.surjective, h.is_compact_image], + apply compact_space.is_compact_univ } } protected lemma t0_space [t0_space α] (h : α ≃ₜ β) : t0_space β := h.symm.embedding.t0_space diff --git a/src/topology/metric_space/antilipschitz.lean b/src/topology/metric_space/antilipschitz.lean index e7b09f09554a2..05db82f6f4b9a 100644 --- a/src/topology/metric_space/antilipschitz.lean +++ b/src/topology/metric_space/antilipschitz.lean @@ -211,7 +211,7 @@ begin let K := f ⁻¹' (closed_ball x₀ r), have A : is_closed K := is_closed_ball.preimage f_cont, have B : bounded K := hK.bounded_preimage bounded_closed_ball, - have : is_compact K := compact_iff_closed_bounded.2 ⟨A, B⟩, + have : is_compact K := is_compact_iff_is_closed_bounded.2 ⟨A, B⟩, convert this.image f_cont, exact (hf.image_preimage _).symm end diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 6da803bf8461c..8390d4399d5ae 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -1944,7 +1944,8 @@ export proper_space (is_compact_closed_ball) /-- In a proper pseudometric space, all spheres are compact. -/ lemma is_compact_sphere {α : Type*} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) : is_compact (sphere x r) := -compact_of_is_closed_subset (is_compact_closed_ball x r) is_closed_sphere sphere_subset_closed_ball +is_compact_of_is_closed_subset (is_compact_closed_ball x r) is_closed_sphere +sphere_subset_closed_ball /-- In a proper pseudometric space, any sphere is a `compact_space` when considered as a subtype. -/ instance {α : Type*} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) : @@ -2013,7 +2014,7 @@ instance complete_of_proper [proper_space α] : complete_space α := (metric.cauchy_iff.1 hf).2 1 zero_lt_one, rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩, have : closed_ball x 1 ∈ f := mem_of_superset t_fset (λ y yt, (ht y yt x xt).le), - rcases (compact_iff_totally_bounded_complete.1 (is_compact_closed_ball x 1)).2 f hf + rcases (is_compact_iff_totally_bounded_is_complete.1 (is_compact_closed_ball x 1)).2 f hf (le_principal_iff.2 this) with ⟨y, -, hy⟩, exact ⟨y, hy⟩ end⟩ @@ -2038,7 +2039,7 @@ begin unfreezingI { rcases eq_empty_or_nonempty s with rfl|hne }, { exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩ }, have : is_compact s, - from compact_of_is_closed_subset (is_compact_closed_ball x r) hs + from is_compact_of_is_closed_subset (is_compact_closed_ball x r) hs (subset.trans h ball_subset_closed_ball), obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closed_ball x (dist y x), from this.exists_forall_ge hne (continuous_id.dist continuous_const).continuous_on, @@ -2268,10 +2269,9 @@ bounded_range_of_tendsto_cofinite_uniformity $ /-- In a compact space, all sets are bounded -/ lemma bounded_of_compact_space [compact_space α] : bounded s := -compact_univ.bounded.mono (subset_univ _) +is_compact_univ.bounded.mono (subset_univ _) -lemma bounded_range_of_tendsto {α : Type*} [pseudo_metric_space α] (u : ℕ → α) {x : α} - (hu : tendsto u at_top (𝓝 x)) : +lemma bounded_range_of_tendsto (u : ℕ → α) {x : α} (hu : tendsto u at_top (𝓝 x)) : bounded (range u) := hu.cauchy_seq.bounded_range @@ -2282,7 +2282,7 @@ begin unfreezingI { rcases eq_empty_or_nonempty s with (rfl|⟨x, hx⟩) }, { exact is_compact_empty }, { rcases hb.subset_ball x with ⟨r, hr⟩, - exact compact_of_is_closed_subset (is_compact_closed_ball x r) hc hr } + exact is_compact_of_is_closed_subset (is_compact_closed_ball x r) hc hr } end /-- The **Heine–Borel theorem**: In a proper space, the closure of a bounded set is compact. -/ @@ -2292,7 +2292,7 @@ is_compact_of_is_closed_bounded is_closed_closure h.closure /-- The **Heine–Borel theorem**: In a proper Hausdorff space, a set is compact if and only if it is closed and bounded. -/ -lemma compact_iff_closed_bounded [t2_space α] [proper_space α] : +lemma is_compact_iff_is_closed_bounded [t2_space α] [proper_space α] : is_compact s ↔ is_closed s ∧ bounded s := ⟨λ h, ⟨h.is_closed, h.bounded⟩, λ h, is_compact_of_is_closed_bounded h.1 h.2⟩ diff --git a/src/topology/metric_space/closeds.lean b/src/topology/metric_space/closeds.lean index 8b4154d495cc3..e08a06bb4a4bd 100644 --- a/src/topology/metric_space/closeds.lean +++ b/src/topology/metric_space/closeds.lean @@ -188,11 +188,12 @@ instance closeds.compact_space [compact_space α] : compact_space (closeds α) : i.e., for all ε>0, there is a finite set which is ε-dense. start from a set `s` which is ε-dense in α. Then the subsets of `s` are finitely many, and ε-dense for the Hausdorff distance. -/ - refine compact_of_totally_bounded_is_closed (emetric.totally_bounded_iff.2 (λε εpos, _)) + refine is_compact_of_totally_bounded_is_closed (emetric.totally_bounded_iff.2 (λε εpos, _)) is_closed_univ, 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⟩, + (is_compact_iff_totally_bounded_is_complete.1 (@is_compact_univ α _ _)).1 δ δpos + with ⟨s, fs, hs⟩, -- 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 ≤ δ, @@ -262,13 +263,13 @@ begin rw edist_comm at Dst, -- since `t` is nonempty, so is `s` exact nonempty_of_Hausdorff_edist_ne_top ht.1 (ne_of_lt Dst) }, - { refine compact_iff_totally_bounded_complete.2 ⟨_, s.closed.is_complete⟩, + { refine is_compact_iff_totally_bounded_is_complete.2 ⟨_, s.closed.is_complete⟩, refine totally_bounded_iff.2 (λε (εpos : 0 < ε), _), -- we have to show that s is covered by finitely many eballs of radius ε -- pick a nonempty compact set t at distance at most ε/2 of s rcases mem_closure_iff.1 hs (ε/2) (ennreal.half_pos εpos.ne') with ⟨t, ht, Dst⟩, -- cover this space with finitely many balls of radius ε/2 - rcases totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 ht.2).1 (ε/2) + rcases totally_bounded_iff.1 (is_compact_iff_totally_bounded_is_complete.1 ht.2).1 (ε/2) (ennreal.half_pos εpos.ne') with ⟨u, fu, ut⟩, refine ⟨u, ⟨fu, λx hx, _⟩⟩, -- u : set α, fu : u.finite, ut : t ⊆ ⋃ (y : α) (H : y ∈ u), eball y (ε / 2) diff --git a/src/topology/metric_space/gromov_hausdorff.lean b/src/topology/metric_space/gromov_hausdorff.lean index c91e2bde6a02c..092a76e9be846 100644 --- a/src/topology/metric_space/gromov_hausdorff.lean +++ b/src/topology/metric_space/gromov_hausdorff.lean @@ -603,7 +603,7 @@ begin have εpos : 0 < ε := mul_pos (by norm_num) δpos, have : ∀ p:GH_space, ∃ s : set p.rep, s.finite ∧ (univ ⊆ (⋃x∈s, ball x ε)) := λ p, by simpa only [subset_univ, exists_true_left] - using finite_cover_balls_of_compact compact_univ εpos, + using finite_cover_balls_of_compact is_compact_univ ε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, @@ -834,7 +834,7 @@ begin refine min_eq_right (nat.floor_mono _), refine mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) ((inv_pos.2 εpos).le), change dist (x : p.rep) y ≤ C, - refine le_trans (dist_le_diam_of_mem compact_univ.bounded (mem_univ _) (mem_univ _)) _, + refine le_trans (dist_le_diam_of_mem is_compact_univ.bounded (mem_univ _) (mem_univ _)) _, exact hdiam p pt end, -- Express `dist (Φ x) (Φ y)` in terms of `F q` @@ -848,7 +848,7 @@ begin refine min_eq_right (nat.floor_mono _), refine mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) ((inv_pos.2 εpos).le), change dist (Ψ x : q.rep) (Ψ y) ≤ C, - refine le_trans (dist_le_diam_of_mem compact_univ.bounded (mem_univ _) (mem_univ _)) _, + refine le_trans (dist_le_diam_of_mem is_compact_univ.bounded (mem_univ _) (mem_univ _)) _, exact hdiam q qt end, -- use the equality between `F p` and `F q` to deduce that the distances have equal diff --git a/src/topology/metric_space/gromov_hausdorff_realized.lean b/src/topology/metric_space/gromov_hausdorff_realized.lean index 1d8bfd5f457e4..1245c6d4a86c0 100644 --- a/src/topology/metric_space/gromov_hausdorff_realized.lean +++ b/src/topology/metric_space/gromov_hausdorff_realized.lean @@ -258,7 +258,7 @@ begin end /-- Compactness of candidates (in bounded_continuous_functions) follows. -/ -private lemma compact_candidates_b : is_compact (candidates_b X Y) := +private lemma is_compact_candidates_b : is_compact (candidates_b X Y) := begin refine arzela_ascoli₂ (Icc 0 (max_var X Y)) is_compact_Icc (candidates_b X Y) closed_candidates_b _ _, @@ -428,7 +428,7 @@ variables (X : Type u) (Y : Type v) [metric_space X] [compact_space X] [nonempty we can finally select a candidate minimizing HD. This will be the candidate realizing the optimal coupling. -/ private lemma exists_minimizer : ∃ f ∈ candidates_b X Y, ∀ g ∈ candidates_b X Y, HD f ≤ HD g := -compact_candidates_b.exists_forall_le candidates_b_nonempty HD_continuous.continuous_on +is_compact_candidates_b.exists_forall_le candidates_b_nonempty HD_continuous.continuous_on private definition optimal_GH_dist : Cb X Y := classical.some (exists_minimizer X Y) @@ -492,8 +492,8 @@ instance compact_space_optimal_GH_coupling : compact_space (optimal_GH_coupling rw this, exact mem_union_right _ (mem_image_of_mem _ (mem_univ _)) } }, rw this, - exact (compact_univ.image (isometry_optimal_GH_injl X Y).continuous).union - (compact_univ.image (isometry_optimal_GH_injr X Y).continuous) + exact (is_compact_univ.image (isometry_optimal_GH_injl X Y).continuous).union + (is_compact_univ.image (isometry_optimal_GH_injr X Y).continuous) end⟩ /-- For any candidate `f`, `HD(f)` is larger than or equal to the Hausdorff distance in the diff --git a/src/topology/noetherian_space.lean b/src/topology/noetherian_space.lean index 79625b2a697d5..56e0a0f2964aa 100644 --- a/src/topology/noetherian_space.lean +++ b/src/topology/noetherian_space.lean @@ -159,7 +159,7 @@ begin simp_rw noetherian_space_set_iff at hf ⊢, intros t ht, rw [← set.inter_eq_left_iff_subset.mpr ht, set.inter_Union], - exact compact_Union (λ i, hf i _ (set.inter_subset_right _ _)) + exact is_compact_Union (λ i, hf i _ (set.inter_subset_right _ _)) end -- This is not an instance since it makes a loop with `t2_space_discrete`. diff --git a/src/topology/paracompact.lean b/src/topology/paracompact.lean index 2dac44fc41ac6..9d7533a5e6320 100644 --- a/src/topology/paracompact.lean +++ b/src/topology/paracompact.lean @@ -109,7 +109,7 @@ instance paracompact_of_compact [compact_space X] : paracompact_space X := begin -- the proof is trivial: we choose a finite subcover using compactness, and use it refine ⟨λ ι s ho hu, _⟩, - rcases compact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩, + rcases is_compact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩, have := hT, simp only [subset_def, mem_Union] at this, choose i hiT hi using λ x, this x (mem_univ x), refine ⟨(T : set ι), λ t, s t, λ t, ho _, _, locally_finite_of_finite _, λ t, ⟨t, subset.rfl⟩⟩, diff --git a/src/topology/separation.lean b/src/topology/separation.lean index ab5e79dc20aeb..5ccc3bea5e8c6 100644 --- a/src/topology/separation.lean +++ b/src/topology/separation.lean @@ -375,7 +375,7 @@ begin split, { rintros ⟨t, ht₁, ht₂, hst⟩, rw compl_subset_compl at hst, - exact compact_of_is_closed_subset ht₂ is_closed_closure (closure_minimal hst ht₁) }, + exact is_compact_of_is_closed_subset ht₂ is_closed_closure (closure_minimal hst ht₁) }, { intros h, exact ⟨closure s, is_closed_closure, h, compl_subset_compl.mpr subset_closure⟩ } end @@ -1138,7 +1138,7 @@ lemma function.left_inverse.closed_embedding [t2_space α] {f : α → β} {g : closed_embedding g := ⟨h.embedding hf hg, h.closed_range hf hg⟩ -lemma compact_compact_separated [t2_space α] {s t : set α} +lemma is_compact_is_compact_separated [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) (hst : disjoint s t) : separated_nhds s t := by simp only [separated_nhds, prod_subset_compl_diagonal_iff_disjoint.symm] at ⊢ hst; @@ -1148,7 +1148,7 @@ by simp only [separated_nhds, prod_subset_compl_diagonal_iff_disjoint.symm] at lemma is_compact.is_closed [t2_space α] {s : set α} (hs : is_compact s) : is_closed s := is_open_compl_iff.1 $ is_open_iff_forall_mem_open.mpr $ assume x hx, let ⟨u, v, uo, vo, su, xv, uv⟩ := - compact_compact_separated hs is_compact_singleton (disjoint_singleton_right.2 hx) in + is_compact_is_compact_separated hs is_compact_singleton (disjoint_singleton_right.2 hx) in ⟨v, (uv.mono_left $ show s ≤ u, from su).subset_compl_left, vo, by simpa using xv⟩ @[simp] lemma filter.coclosed_compact_eq_cocompact [t2_space α] : @@ -1163,10 +1163,10 @@ by rw bornology.ext_iff; exact filter.coclosed_compact_eq_cocompact `⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhd_of_compact'` where we don't need to assume each `V i` closed because it follows from compactness since `α` is assumed to be Hausdorff. -/ -lemma exists_subset_nhd_of_compact [t2_space α] {ι : Type*} [nonempty ι] {V : ι → set α} +lemma exists_subset_nhds_of_is_compact [t2_space α] {ι : Type*} [nonempty ι] {V : ι → set α} (hV : directed (⊇) V) (hV_cpct : ∀ i, is_compact (V i)) {U : set α} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U := -exists_subset_nhd_of_compact' hV hV_cpct (λ i, (hV_cpct i).is_closed) hU +exists_subset_nhds_of_is_compact' hV hV_cpct (λ i, (hV_cpct i).is_closed) hU lemma compact_exhaustion.is_closed [t2_space α] (K : compact_exhaustion α) (n : ℕ) : is_closed (K n) := @@ -1176,16 +1176,16 @@ lemma is_compact.inter [t2_space α] {s t : set α} (hs : is_compact s) (ht : is is_compact (s ∩ t) := hs.inter_right $ ht.is_closed -lemma compact_closure_of_subset_compact [t2_space α] {s t : set α} (ht : is_compact t) (h : s ⊆ t) : - is_compact (closure s) := -compact_of_is_closed_subset ht is_closed_closure (closure_minimal h ht.is_closed) +lemma is_compact_closure_of_subset_compact [t2_space α] {s t : set α} + (ht : is_compact t) (h : s ⊆ t) : is_compact (closure s) := +is_compact_of_is_closed_subset ht is_closed_closure (closure_minimal h ht.is_closed) @[simp] lemma exists_compact_superset_iff [t2_space α] {s : set α} : (∃ K, is_compact K ∧ s ⊆ K) ↔ is_compact (closure s) := -⟨λ ⟨K, hK, hsK⟩, compact_closure_of_subset_compact hK hsK, λ h, ⟨closure s, h, subset_closure⟩⟩ +⟨λ ⟨K, hK, hsK⟩, is_compact_closure_of_subset_compact hK hsK, λ h, ⟨closure s, h, subset_closure⟩⟩ -lemma image_closure_of_compact [t2_space β] +lemma image_closure_of_is_compact [t2_space β] {s : set α} (hs : is_compact (closure s)) {f : α → β} (hf : continuous_on f (closure s)) : f '' closure s = closure (f '' s) := subset.antisymm hf.image_closure $ closure_minimal (image_subset f subset_closure) @@ -1196,7 +1196,8 @@ lemma is_compact.binary_compact_cover [t2_space α] {K U V : set α} (hK : is_co (hU : is_open U) (hV : is_open V) (h2K : K ⊆ U ∪ V) : ∃ K₁ K₂ : set α, is_compact K₁ ∧ is_compact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ := begin - obtain ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩ := compact_compact_separated (hK.diff hU) (hK.diff hV) + obtain ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩ := + is_compact_is_compact_separated (hK.diff hU) (hK.diff hV) (by rwa [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]), exact ⟨_, _, hK.diff h1O₁, hK.diff h1O₂, by rwa [diff_subset_comm], by rwa [diff_subset_comm], by rw [← diff_inter, hO.inter_eq, diff_empty]⟩ @@ -1247,7 +1248,8 @@ lemma locally_compact_of_compact_nhds [t2_space α] (h : ∀ x : α, ∃ s, s -- K \ U is again compact and doesn't contain x, so -- we may find open sets V, W separating x from K \ U. -- Then K \ W is a compact neighborhood of x contained in U. - let ⟨v, w, vo, wo, xv, kuw, vw⟩ := compact_compact_separated is_compact_singleton (kc.diff uo) + let ⟨v, w, vo, wo, xv, kuw, vw⟩ := + is_compact_is_compact_separated is_compact_singleton (kc.diff uo) (disjoint_singleton_left.2 $ λ h, h.2 xu) in have wn : wᶜ ∈ 𝓝 x, from mem_nhds_iff.mpr ⟨v, vw.subset_compl_right, vo, singleton_subset_iff.mp xv⟩, @@ -1258,7 +1260,7 @@ lemma locally_compact_of_compact_nhds [t2_space α] (h : ∀ x : α, ∃ s, s @[priority 100] -- see Note [lower instance priority] instance locally_compact_of_compact [t2_space α] [compact_space α] : locally_compact_space α := -locally_compact_of_compact_nhds (assume x, ⟨univ, is_open_univ.mem_nhds trivial, compact_univ⟩) +locally_compact_of_compact_nhds (assume x, ⟨univ, is_open_univ.mem_nhds trivial, is_compact_univ⟩) /-- In a locally compact T₂ space, every point has an open neighborhood with compact closure -/ lemma exists_open_with_compact_closure [locally_compact_space α] [t2_space α] (x : α) : @@ -1266,7 +1268,7 @@ lemma exists_open_with_compact_closure [locally_compact_space α] [t2_space α] begin rcases exists_compact_mem_nhds x with ⟨K, hKc, hxK⟩, rcases mem_nhds_iff.1 hxK with ⟨t, h1t, h2t, h3t⟩, - exact ⟨t, h2t, h3t, compact_closure_of_subset_compact hKc h1t⟩ + exact ⟨t, h2t, h3t, is_compact_closure_of_subset_compact hKc h1t⟩ end /-- @@ -1277,7 +1279,7 @@ lemma exists_open_superset_and_is_compact_closure [locally_compact_space α] [t2 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⟩, + is_compact_closure_of_subset_compact hK' interior_subset⟩, end /-- @@ -1291,7 +1293,7 @@ begin rcases exists_compact_between hK hU hKU with ⟨V, hV, hKV, hVU⟩, exact ⟨interior V, is_open_interior, hKV, (closure_minimal interior_subset hV.is_closed).trans hVU, - compact_closure_of_subset_compact hV interior_subset⟩, + is_compact_closure_of_subset_compact hV interior_subset⟩, end lemma is_preirreducible_iff_subsingleton [t2_space α] {S : set α} : @@ -1559,7 +1561,7 @@ instance normal_space.t3_space [normal_space α] : t3_space α := -- We can't make this an instance because it could cause an instance loop. lemma normal_of_compact_t2 [compact_space α] [t2_space α] : normal_space α := -⟨λ s t hs ht, compact_compact_separated hs.is_compact ht.is_compact⟩ +⟨λ s t hs ht, is_compact_is_compact_separated hs.is_compact ht.is_compact⟩ protected lemma closed_embedding.normal_space [topological_space β] [normal_space β] {f : α → β} (hf : closed_embedding f) : normal_space α := @@ -1816,7 +1818,7 @@ lemma nhds_basis_clopen (x : α) : (𝓝 x).has_basis (λ s : set α, x ∈ s { intros y y_in, erw [this, mem_singleton_iff] at y_in, rwa y_in }, - exact exists_subset_nhd_of_compact_space hdir hNcl h_nhd }, + exact exists_subset_nhds_of_compact_space hdir hNcl h_nhd }, { rintro ⟨V, ⟨hxV, V_op, -⟩, hUV : V ⊆ U⟩, rw mem_nhds_iff, exact ⟨V, hUV, V_op, hxV⟩ } @@ -1836,8 +1838,8 @@ end /-- Every member of an open set in a compact Hausdorff totally disconnected space is contained in a clopen set contained in the open set. -/ lemma compact_exists_clopen_in_open {x : α} {U : set α} (is_open : is_open U) (memU : x ∈ U) : - ∃ (V : set α) (hV : is_clopen V), x ∈ V ∧ V ⊆ U := - (is_topological_basis.mem_nhds_iff is_topological_basis_clopen).1 (is_open.mem_nhds memU) + ∃ (V : set α) (hV : is_clopen V), x ∈ V ∧ V ⊆ U := +(is_topological_basis.mem_nhds_iff is_topological_basis_clopen).1 (is_open.mem_nhds memU) end profinite diff --git a/src/topology/sequences.lean b/src/topology/sequences.lean index c6637f97752f5..1ac8114a45084 100644 --- a/src/topology/sequences.lean +++ b/src/topology/sequences.lean @@ -268,7 +268,7 @@ hs.is_seq_compact hx @[priority 100] -- see Note [lower instance priority] instance first_countable_topology.seq_compact_of_compact [compact_space X] : seq_compact_space X := -⟨compact_univ.is_seq_compact⟩ +⟨is_compact_univ.is_seq_compact⟩ lemma compact_space.tendsto_subseq [compact_space X] (x : ℕ → X) : ∃ a (φ : ℕ → ℕ), strict_mono φ ∧ tendsto (x ∘ φ) at_top (𝓝 a) := @@ -385,13 +385,14 @@ end /-- A version of Bolzano-Weistrass: in a uniform space with countably generated uniformity filter (e.g., in a metric space), a set is compact if and only if it is sequentially compact. -/ -protected lemma uniform_space.compact_iff_seq_compact [is_countably_generated $ 𝓤 X] : +protected lemma uniform_space.is_compact_iff_is_seq_compact [is_countably_generated $ 𝓤 X] : is_compact s ↔ is_seq_compact s := ⟨λ H, H.is_seq_compact, λ H, H.is_compact⟩ lemma uniform_space.compact_space_iff_seq_compact_space [is_countably_generated $ 𝓤 X] : compact_space X ↔ seq_compact_space X := -have key : is_compact (univ : set X) ↔ is_seq_compact univ := uniform_space.compact_iff_seq_compact, +have key : is_compact (univ : set X) ↔ is_seq_compact univ := + uniform_space.is_compact_iff_is_seq_compact, ⟨λ ⟨h⟩, ⟨key.mp h⟩, λ ⟨h⟩, ⟨key.mpr h⟩⟩ end uniform_space_seq_compact diff --git a/src/topology/sets/compacts.lean b/src/topology/sets/compacts.lean index 0524ac1ac956c..28b0a6f2f6df4 100644 --- a/src/topology/sets/compacts.lean +++ b/src/topology/sets/compacts.lean @@ -56,7 +56,7 @@ instance : can_lift (set α) (compacts α) coe is_compact := instance : has_sup (compacts α) := ⟨λ s t, ⟨s ∪ t, s.is_compact.union t.is_compact⟩⟩ instance [t2_space α] : has_inf (compacts α) := ⟨λ s t, ⟨s ∩ t, s.is_compact.inter t.is_compact⟩⟩ -instance [compact_space α] : has_top (compacts α) := ⟨⟨univ, compact_univ⟩⟩ +instance [compact_space α] : has_top (compacts α) := ⟨⟨univ, is_compact_univ⟩⟩ instance : has_bot (compacts α) := ⟨⟨∅, is_compact_empty⟩⟩ instance : semilattice_sup (compacts α) := set_like.coe_injective.semilattice_sup _ (λ _ _, rfl) diff --git a/src/topology/spectral/hom.lean b/src/topology/spectral/hom.lean index 0b44d6ad54dae..065bd5fabd165 100644 --- a/src/topology/spectral/hom.lean +++ b/src/topology/spectral/hom.lean @@ -32,11 +32,11 @@ variables [topological_space α] [topological_space β] [topological_space γ] { /-- A function between topological spaces is spectral if it is continuous and the preimage of every compact open set is compact open. -/ structure is_spectral_map (f : α → β) extends continuous f : Prop := -(compact_preimage_of_open ⦃s : set β⦄ : is_open s → is_compact s → is_compact (f ⁻¹' s)) +(is_compact_preimage_of_is_open ⦃s : set β⦄ : is_open s → is_compact s → is_compact (f ⁻¹' s)) -lemma is_compact.preimage_of_open (hf : is_spectral_map f) (h₀ : is_compact s) (h₁ : is_open s) : +lemma is_compact.preimage_of_is_open (hf : is_spectral_map f) (h₀ : is_compact s) (h₁ : is_open s) : is_compact (f ⁻¹' s) := -hf.compact_preimage_of_open h₁ h₀ +hf.is_compact_preimage_of_is_open h₁ h₀ lemma is_spectral_map.continuous {f : α → β} (hf : is_spectral_map f) : continuous f := hf.to_continuous @@ -47,7 +47,7 @@ lemma is_spectral_map.comp {f : β → γ} {g : α → β} (hf : is_spectral_map (hg : is_spectral_map g) : is_spectral_map (f ∘ g) := ⟨hf.continuous.comp hg.continuous, - λ s hs₀ hs₁, (hs₁.preimage_of_open hf hs₀).preimage_of_open hg (hs₀.preimage hf.continuous)⟩ + λ s hs₀ hs₁, (hs₁.preimage_of_is_open hf hs₀).preimage_of_is_open hg (hs₀.preimage hf.continuous)⟩ end unbundled diff --git a/src/topology/stone_cech.lean b/src/topology/stone_cech.lean index 4f93bb4abf2a2..8f8340bd77ad6 100644 --- a/src/topology/stone_cech.lean +++ b/src/topology/stone_cech.lean @@ -176,7 +176,7 @@ variables [compact_space γ] lemma continuous_ultrafilter_extend (f : α → γ) : continuous (ultrafilter.extend f) := have ∀ (b : ultrafilter α), ∃ c, tendsto f (comap pure (𝓝 b)) (𝓝 c) := assume b, -- b.map f is an ultrafilter on γ, which is compact, so it converges to some c in γ. - let ⟨c, _, h⟩ := compact_univ.ultrafilter_le_nhds (b.map f) + let ⟨c, _, h⟩ := is_compact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem) in ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h⟩, begin diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 39a28124c0816..9e66e953bcec4 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -123,7 +123,7 @@ lemma is_compact.diff (hs : is_compact s) (ht : is_open t) : is_compact (s \ t) hs.inter_right (is_closed_compl_iff.mpr ht) /-- A closed subset of a compact set is a compact set. -/ -lemma compact_of_is_closed_subset (hs : is_compact s) (ht : is_closed t) (h : t ⊆ s) : +lemma is_compact_of_is_closed_subset (hs : is_compact s) (ht : is_closed t) (h : t ⊆ s) : is_compact t := inter_eq_self_of_subset_right h ▸ hs.inter_right ht @@ -299,7 +299,8 @@ lemma is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed have Zmono : antitone Z := antitone_nat_of_succ_le hZd, have hZd : directed (⊇) Z, from directed_of_sup Zmono, have ∀ i, Z i ⊆ Z 0, from assume i, Zmono $ zero_le i, -have hZc : ∀ i, is_compact (Z i), from assume i, compact_of_is_closed_subset hZ0 (hZcl i) (this i), +have hZc : ∀ i, is_compact (Z i), + from assume i, is_compact_of_is_closed_subset hZ0 (hZcl i) (this i), 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. -/ @@ -409,7 +410,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 : s.finite) +lemma set.finite.is_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, @@ -427,20 +428,20 @@ is_compact_of_finite_subcover $ assume ι U hUo hsU, 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)) : +lemma finset.is_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 +s.finite_to_set.is_compact_bUnion hf -lemma compact_accumulate {K : ℕ → set α} (hK : ∀ n, is_compact (K n)) (n : ℕ) : +lemma is_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 +(finite_le_nat n).is_compact_bUnion $ λ k _, hK k -lemma compact_Union {f : ι → set α} [finite ι] (h : ∀ i, is_compact (f i)) : +lemma is_compact_Union {f : ι → set α} [finite ι] (h : ∀ i, is_compact (f i)) : is_compact (⋃ i, f i) := -by rw ← bUnion_univ; exact finite_univ.compact_bUnion (λ i _, h i) +by rw ← bUnion_univ; exact finite_univ.is_compact_bUnion (λ i _, h i) lemma set.finite.is_compact (hs : s.finite) : is_compact s := -bUnion_of_singleton s ▸ hs.compact_bUnion (λ _ _, is_compact_singleton) +bUnion_of_singleton s ▸ hs.is_compact_bUnion (λ _ _, is_compact_singleton) lemma is_compact.finite_of_discrete [discrete_topology α] {s : set α} (hs : is_compact s) : s.finite := @@ -455,7 +456,7 @@ lemma is_compact_iff_finite [discrete_topology α] {s : set α} : is_compact s ⟨λ h, h.finite_of_discrete, λ h, h.is_compact⟩ lemma is_compact.union (hs : is_compact s) (ht : is_compact t) : is_compact (s ∪ t) := -by rw union_eq_Union; exact compact_Union (λ b, by cases b; assumption) +by rw union_eq_Union; exact is_compact_Union (λ b, by cases b; assumption) lemma is_compact.insert (hs : is_compact s) (a) : is_compact (insert a s) := is_compact_singleton.union hs @@ -463,7 +464,8 @@ is_compact_singleton.union hs /-- If `V : ι → set α` is a decreasing family of closed compact sets then any neighborhood of `⋂ i, V i` contains some `V i`. We assume each `V i` is compact *and* closed because `α` is not assumed to be Hausdorff. See `exists_subset_nhd_of_compact` for version assuming this. -/ -lemma exists_subset_nhd_of_compact' {ι : Type*} [nonempty ι] {V : ι → set α} (hV : directed (⊇) V) +lemma exists_subset_nhds_of_is_compact' {ι : Type*} [nonempty ι] + {V : ι → set α} (hV : directed (⊇) V) (hV_cpct : ∀ i, is_compact (V i)) (hV_closed : ∀ i, is_closed (V i)) {U : set α} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U := begin @@ -510,7 +512,7 @@ begin exact set.subset_Union (b ∘ f') j } }, { rintro ⟨s, hs, rfl⟩, split, - { exact hs.compact_bUnion (λ i _, hb' i) }, + { exact hs.is_compact_bUnion (λ i _, hb' i) }, { apply is_open_bUnion, intros i hi, exact hb.is_open (set.mem_range_self _) } }, end @@ -700,7 +702,7 @@ end tube_lemma /-- Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here. -/ class compact_space (α : Type*) [topological_space α] : Prop := -(compact_univ : is_compact (univ : set α)) +(is_compact_univ : is_compact (univ : set α)) @[priority 10] -- see Note [lower instance priority] instance subsingleton.compact_space [subsingleton α] : compact_space α := @@ -708,17 +710,17 @@ instance subsingleton.compact_space [subsingleton α] : compact_space α := lemma is_compact_univ_iff : is_compact (univ : set α) ↔ compact_space α := ⟨λ h, ⟨h⟩, λ h, h.1⟩ -lemma compact_univ [h : compact_space α] : is_compact (univ : set α) := h.compact_univ +lemma is_compact_univ [h : compact_space α] : is_compact (univ : set α) := h.is_compact_univ 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) +by simpa using is_compact_univ (show f ≤ 𝓟 univ, by simp) lemma compact_space.elim_nhds_subcover [compact_space α] (U : α → set α) (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : finset α, (⋃ x ∈ t, U x) = ⊤ := begin - obtain ⟨t, -, s⟩ := is_compact.elim_nhds_subcover compact_univ U (λ x m, hU x), + obtain ⟨t, -, s⟩ := is_compact.elim_nhds_subcover is_compact_univ U (λ x m, hU x), exact ⟨t, by { rw eq_top_iff, exact s }⟩, end @@ -726,7 +728,7 @@ 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 α := -{ compact_univ := +{ is_compact_univ := begin apply is_compact_of_finite_subfamily_closed, intros ι Z, specialize h Z, @@ -735,7 +737,7 @@ theorem compact_space_of_finite_subfamily_closed lemma is_closed.is_compact [compact_space α] {s : set α} (h : is_closed s) : is_compact s := -compact_of_is_closed_subset compact_univ h (subset_univ _) +is_compact_of_is_closed_subset is_compact_univ h (subset_univ _) /-- `α` is a noncompact topological space if it not a compact space. -/ class noncompact_space (α : Type*) [topological_space α] : Prop := @@ -755,7 +757,7 @@ end @[simp] lemma filter.cocompact_eq_bot [compact_space α] : filter.cocompact α = ⊥ := -filter.has_basis_cocompact.eq_bot_iff.mpr ⟨set.univ, compact_univ, set.compl_univ⟩ +filter.has_basis_cocompact.eq_bot_iff.mpr ⟨set.univ, is_compact_univ, set.compl_univ⟩ instance [noncompact_space α] : ne_bot (filter.coclosed_compact α) := ne_bot_of_le filter.cocompact_le_coclosed_compact @@ -775,7 +777,7 @@ noncompact_space_of_ne_bot $ by simp only [filter.cocompact_eq_cofinite, filter. -- Note: We can't make this into an instance because it loops with `finite.compact_space`. /-- A compact discrete space is finite. -/ lemma finite_of_compact_of_discrete [compact_space α] [discrete_topology α] : finite α := -finite.of_finite_univ $ compact_univ.finite_of_discrete +finite.of_finite_univ $ is_compact_univ.finite_of_discrete lemma exists_nhds_ne_ne_bot (α : Type*) [topological_space α] [compact_space α] [infinite α] : ∃ z : α, (𝓝[≠] z).ne_bot := @@ -788,7 +790,7 @@ end lemma finite_cover_nhds_interior [compact_space α] {U : α → set α} (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : finset α, (⋃ x ∈ t, interior (U x)) = univ := -let ⟨t, ht⟩ := compact_univ.elim_finite_subcover (λ x, interior (U x)) (λ x, is_open_interior) +let ⟨t, ht⟩ := is_compact_univ.elim_finite_subcover (λ x, interior (U x)) (λ x, is_open_interior) (λ x _, mem_Union.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩) in ⟨t, univ_subset_iff.1 ht⟩ @@ -802,7 +804,7 @@ many nonempty elements. -/ lemma locally_finite.finite_nonempty_of_compact {ι : Type*} [compact_space α] {f : ι → set α} (hf : locally_finite f) : {i | (f i).nonempty}.finite := -by simpa only [inter_univ] using hf.finite_nonempty_inter_compact compact_univ +by simpa only [inter_univ] using hf.finite_nonempty_inter_compact is_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. -/ @@ -832,7 +834,7 @@ end lemma is_compact_range [compact_space α] {f : α → β} (hf : continuous f) : is_compact (range f) := -by rw ← image_univ; exact compact_univ.image hf +by rw ← image_univ; exact is_compact_univ.image hf lemma is_compact_diagonal [compact_space α] : is_compact (diagonal α) := @range_diag α ▸ is_compact_range (continuous_id.prod_mk continuous_id) @@ -868,10 +870,10 @@ begin ... = 𝓝 x ⊓ map πX (comap πY (𝓝 y) ⊓ 𝓟 C) : by rw inf_comm end -lemma exists_subset_nhd_of_compact_space [compact_space α] {ι : Type*} [nonempty ι] +lemma exists_subset_nhds_of_compact_space [compact_space α] {ι : Type*} [nonempty ι] {V : ι → set α} (hV : directed (⊇) V) (hV_closed : ∀ i, is_closed (V i)) {U : set α} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U := -exists_subset_nhd_of_compact' hV (λ i, (hV_closed i).is_compact) hV_closed hU +exists_subset_nhds_of_is_compact' hV (λ i, (hV_closed i).is_compact) hV_closed hU /-- If `f : α → β` is an `inducing` map, then the image `f '' s` of a set `s` is compact if and only if the set `s` is closed. -/ @@ -911,15 +913,15 @@ lemma closed_embedding.tendsto_cocompact filter.has_basis_cocompact.tendsto_right_iff.mpr $ λ K hK, (hf.is_compact_preimage hK).compl_mem_cocompact -lemma compact_iff_compact_in_subtype {p : α → Prop} {s : set {a // p a}} : +lemma is_compact_iff_is_compact_in_subtype {p : α → Prop} {s : set {a // p a}} : is_compact s ↔ is_compact ((coe : _ → α) '' s) := embedding_subtype_coe.is_compact_iff_is_compact_image lemma is_compact_iff_is_compact_univ {s : set α} : is_compact s ↔ is_compact (univ : set s) := -by rw [compact_iff_compact_in_subtype, image_univ, subtype.range_coe]; refl +by rw [is_compact_iff_is_compact_in_subtype, image_univ, subtype.range_coe]; refl lemma is_compact_iff_compact_space {s : set α} : is_compact s ↔ compact_space s := -is_compact_iff_is_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.compact_univ _ _⟩ +is_compact_iff_is_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.is_compact_univ _ _⟩ lemma is_compact.finite {s : set α} (hs : is_compact s) (hs' : discrete_topology s) : s.finite := finite_coe_iff.mp (@finite_of_compact_of_discrete _ _ (is_compact_iff_compact_space.mp hs) hs') @@ -958,11 +960,11 @@ end /-- Finite topological spaces are compact. -/ @[priority 100] instance finite.compact_space [finite α] : compact_space α := -{ compact_univ := finite_univ.is_compact } +{ is_compact_univ := finite_univ.is_compact } /-- The product of two compact spaces is compact. -/ instance [compact_space α] [compact_space β] : compact_space (α × β) := -⟨by { rw ← univ_prod_univ, exact compact_univ.prod compact_univ }⟩ +⟨by { rw ← univ_prod_univ, exact is_compact_univ.prod is_compact_univ }⟩ /-- The disjoint union of two compact spaces is compact. -/ instance [compact_space α] [compact_space β] : compact_space (α ⊕ β) := @@ -976,7 +978,7 @@ instance [finite ι] [Π i, topological_space (π i)] [∀ i, compact_space (π begin refine ⟨_⟩, rw sigma.univ, - exact compact_Union (λ i, is_compact_range continuous_sigma_mk), + exact is_compact_Union (λ i, is_compact_range continuous_sigma_mk), end /-- The coproduct of the cocompact filters on two topological spaces is the cocompact filter on @@ -1042,7 +1044,7 @@ lemma is_compact_univ_pi {s : Π i, set (π i)} (h : ∀ i, is_compact (s i)) : by { convert is_compact_pi_infinite h, simp only [← mem_univ_pi, set_of_mem_eq] } instance pi.compact_space [∀ i, compact_space (π i)] : compact_space (Πi, π i) := -⟨by { rw [← pi_univ univ], exact is_compact_univ_pi (λ i, compact_univ) }⟩ +⟨by { rw [← pi_univ univ], exact is_compact_univ_pi (λ i, is_compact_univ) }⟩ /-- **Tychonoff's theorem** formulated in terms of filters: `filter.cocompact` on an indexed product type `Π d, κ d` the `filter.Coprod` of filters `filter.cocompact` on `κ d`. -/ @@ -1122,7 +1124,7 @@ instance locally_compact_space.pi [∀ i, compact_space (π i)] : locally_compac refine is_compact_univ_pi (λ i, _), by_cases i ∈ s, { rw if_pos h, exact hc i, }, - { rw if_neg h, exact compact_space.compact_univ, } }, + { rw if_neg h, exact compact_space.is_compact_univ, } }, end⟩ end pi @@ -1151,7 +1153,7 @@ begin choose V hVc hxV hKV using λ x : K, exists_compact_subset hU (h_KU x.2), have : K ⊆ ⋃ x, interior (V x), from λ x hx, mem_Union.2 ⟨⟨x, hx⟩, hxV _⟩, rcases hK.elim_finite_subcover _ (λ x, @is_open_interior α _ (V x)) this with ⟨t, ht⟩, - refine ⟨_, t.compact_bUnion (λ x _, hVc x), λ x hx, _, set.Union₂_subset (λ i _, hKV i)⟩, + refine ⟨_, t.is_compact_bUnion (λ x _, hVc x), λ x hx, _, set.Union₂_subset (λ i _, hKV i)⟩, rcases mem_Union₂.1 (ht hx) with ⟨y, hyt, hy⟩, exact interior_mono (subset_bUnion_of_mem hyt) hy, end @@ -1195,7 +1197,7 @@ hs.open_embedding_subtype_coe.locally_compact_space lemma ultrafilter.le_nhds_Lim [compact_space α] (F : ultrafilter α) : ↑F ≤ 𝓝 (@Lim _ _ (F : filter α).nonempty_of_ne_bot F) := begin - rcases compact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩, + rcases is_compact_univ.ultrafilter_le_nhds F (by simp) with ⟨x, -, h⟩, exact le_nhds_Lim ⟨x,h⟩, end @@ -1248,7 +1250,7 @@ class sigma_compact_space (α : Type*) [topological_space α] : Prop := @[priority 200] -- see Note [lower instance priority] instance compact_space.sigma_compact [compact_space α] : sigma_compact_space α := -⟨⟨λ _, univ, λ _, compact_univ, Union_const _⟩⟩ +⟨⟨λ _, univ, λ _, is_compact_univ, Union_const _⟩⟩ lemma sigma_compact_space.of_countable (S : set (set α)) (Hc : S.countable) (Hcomp : ∀ s ∈ S, is_compact s) (HU : ⋃₀ S = univ) : sigma_compact_space α := @@ -1272,7 +1274,7 @@ def compact_covering : ℕ → set α := accumulate exists_compact_covering.some lemma is_compact_compact_covering (n : ℕ) : is_compact (compact_covering α n) := -compact_accumulate (classical.some_spec sigma_compact_space.exists_compact_covering).1 n +is_compact_accumulate (classical.some_spec sigma_compact_space.exists_compact_covering).1 n lemma Union_compact_covering : (⋃ n, compact_covering α n) = univ := begin diff --git a/src/topology/support.lean b/src/topology/support.lean index bbf5d082b7f87..35b0b9e55261e 100644 --- a/src/topology/support.lean +++ b/src/topology/support.lean @@ -138,7 +138,7 @@ lemma has_compact_mul_support_iff_eventually_eq : ⟨ λ h, mem_coclosed_compact.mpr ⟨mul_tsupport f, is_closed_mul_tsupport _, h, λ x, not_imp_comm.mpr $ λ hx, subset_mul_tsupport f hx⟩, λ h, let ⟨C, hC⟩ := mem_coclosed_compact'.mp h in - compact_of_is_closed_subset hC.2.1 (is_closed_mul_tsupport _) (closure_minimal hC.2.2 hC.1)⟩ + is_compact_of_is_closed_subset hC.2.1 (is_closed_mul_tsupport _) (closure_minimal hC.2.2 hC.1)⟩ @[to_additive] lemma has_compact_mul_support.is_compact_range [topological_space β] @@ -151,7 +151,7 @@ end @[to_additive] lemma has_compact_mul_support.mono' {f' : α → γ} (hf : has_compact_mul_support f) (hff' : mul_support f' ⊆ mul_tsupport f) : has_compact_mul_support f' := -compact_of_is_closed_subset hf is_closed_closure $ closure_minimal hff' is_closed_closure +is_compact_of_is_closed_subset hf is_closed_closure $ closure_minimal hff' is_closed_closure @[to_additive] lemma has_compact_mul_support.mono {f' : α → γ} (hf : has_compact_mul_support f) @@ -173,7 +173,7 @@ lemma has_compact_mul_support.comp_closed_embedding (hf : has_compact_mul_suppor {g : α' → α} (hg : closed_embedding g) : has_compact_mul_support (f ∘ g) := begin rw [has_compact_mul_support_def, function.mul_support_comp_eq_preimage], - refine compact_of_is_closed_subset (hg.is_compact_preimage hf) is_closed_closure _, + refine is_compact_of_is_closed_subset (hg.is_compact_preimage hf) is_closed_closure _, rw [hg.to_embedding.closure_eq_preimage_closure_image], exact preimage_mono (closure_mono $ image_preimage_subset _ _) end diff --git a/src/topology/uniform_space/cauchy.lean b/src/topology/uniform_space/cauchy.lean index 325d9efb2d448..f648dcc997395 100644 --- a/src/topology/uniform_space/cauchy.lean +++ b/src/topology/uniform_space/cauchy.lean @@ -534,7 +534,7 @@ begin exact ⟨ultrafilter.of f, ultrafilter.of_le f, H _ ((ultrafilter.of_le f).trans hfs)⟩ end -lemma compact_iff_totally_bounded_complete {s : set α} : +lemma is_compact_iff_totally_bounded_is_complete {s : set α} : is_compact s ↔ totally_bounded s ∧ is_complete s := ⟨λ hs, ⟨totally_bounded_iff_ultrafilter.2 (λ f hf, let ⟨x, xs, fx⟩ := is_compact_iff_ultrafilter_le_nhds.1 hs f hf in cauchy_nhds.mono fx), @@ -545,18 +545,18 @@ lemma compact_iff_totally_bounded_complete {s : set α} : (λf hf, hc _ (totally_bounded_iff_ultrafilter.1 ht f hf) hf)⟩ protected lemma is_compact.totally_bounded {s : set α} (h : is_compact s) : totally_bounded s := -(compact_iff_totally_bounded_complete.1 h).1 +(is_compact_iff_totally_bounded_is_complete.1 h).1 protected lemma is_compact.is_complete {s : set α} (h : is_compact s) : is_complete s := -(compact_iff_totally_bounded_complete.1 h).2 +(is_compact_iff_totally_bounded_is_complete.1 h).2 @[priority 100] -- see Note [lower instance priority] instance complete_of_compact {α : Type u} [uniform_space α] [compact_space α] : complete_space α := -⟨λf hf, by simpa using (compact_iff_totally_bounded_complete.1 compact_univ).2 f hf⟩ +⟨λf hf, by simpa using (is_compact_iff_totally_bounded_is_complete.1 is_compact_univ).2 f hf⟩ -lemma compact_of_totally_bounded_is_closed [complete_space α] {s : set α} +lemma is_compact_of_totally_bounded_is_closed [complete_space α] {s : set α} (ht : totally_bounded s) (hc : is_closed s) : is_compact s := -(@compact_iff_totally_bounded_complete α _ s).2 ⟨ht, hc.is_complete⟩ +(@is_compact_iff_totally_bounded_is_complete α _ s).2 ⟨ht, hc.is_complete⟩ /-- Every Cauchy sequence over `ℕ` is totally bounded. -/ lemma cauchy_seq.totally_bounded_range {s : ℕ → α} (hs : cauchy_seq s) : diff --git a/src/topology/uniform_space/compact.lean b/src/topology/uniform_space/compact.lean index bd87660593be7..4add27395ac27 100644 --- a/src/topology/uniform_space/compact.lean +++ b/src/topology/uniform_space/compact.lean @@ -210,7 +210,7 @@ lemma continuous_on.tendsto_uniformly [locally_compact_space α] [compact_space begin rcases locally_compact_space.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩, have : uniform_continuous_on ↿f (K ×ˢ univ), - from is_compact.uniform_continuous_on_of_continuous (hK.prod compact_univ) + from is_compact.uniform_continuous_on_of_continuous (hK.prod is_compact_univ) (h.mono $ prod_mono hKU subset.rfl), exact this.tendsto_uniformly hxK end diff --git a/src/topology/uniform_space/compact_convergence.lean b/src/topology/uniform_space/compact_convergence.lean index c2e801812db46..7b3fc75c6ad8b 100644 --- a/src/topology/uniform_space/compact_convergence.lean +++ b/src/topology/uniform_space/compact_convergence.lean @@ -414,7 +414,7 @@ lemma has_basis_compact_convergence_uniformity_of_compact : (λ V, { fg : C(α, β) × C(α, β) | ∀ x, (fg.1 x, fg.2 x) ∈ V }) := has_basis_compact_convergence_uniformity.to_has_basis (λ p hp, ⟨p.2, hp.2, λ fg hfg x hx, hfg x⟩) - (λ V hV, ⟨⟨univ, V⟩, ⟨compact_univ, hV⟩, λ fg hfg x, hfg x (mem_univ x)⟩) + (λ V hV, ⟨⟨univ, V⟩, ⟨is_compact_univ, hV⟩, λ fg hfg x, hfg x (mem_univ x)⟩) /-- Convergence in the compact-open topology is the same as uniform convergence for sequences of continuous functions on a compact space. -/ @@ -422,7 +422,7 @@ lemma tendsto_iff_tendsto_uniformly : tendsto F p (𝓝 f) ↔ tendsto_uniformly (λ i a, F i a) f p := begin rw [tendsto_iff_forall_compact_tendsto_uniformly_on, ← tendsto_uniformly_on_univ], - exact ⟨λ h, h univ compact_univ, λ h K hK, h.mono (subset_univ K)⟩, + exact ⟨λ h, h univ is_compact_univ, λ h K hK, h.mono (subset_univ K)⟩, end end compact_domain diff --git a/src/topology/uniform_space/uniform_convergence.lean b/src/topology/uniform_space/uniform_convergence.lean index 839c640fdafb3..41f6f91dc2f6a 100644 --- a/src/topology/uniform_space/uniform_convergence.lean +++ b/src/topology/uniform_space/uniform_convergence.lean @@ -735,7 +735,7 @@ lemma tendsto_locally_uniformly_iff_tendsto_uniformly_of_compact_space [compact_ begin refine ⟨λ h V hV, _, tendsto_uniformly.tendsto_locally_uniformly⟩, choose U hU using h V hV, - obtain ⟨t, ht⟩ := compact_univ.elim_nhds_subcover' (λ k hk, U k) (λ k hk, (hU k).1), + obtain ⟨t, ht⟩ := is_compact_univ.elim_nhds_subcover' (λ k hk, U k) (λ k hk, (hU k).1), replace hU := λ (x : t), (hU x).2, rw ← eventually_all at hU, refine hU.mono (λ i hi x, _),