chore(topology/*): rename compact_univ to is_compact_univ, and many m…

…ore (#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

@@ -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'

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'

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,

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) :

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,

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)

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
 

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
 

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⟩],

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

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
 

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

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⟩,

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',

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

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
 

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)

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, _⟩,

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

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 }
 

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₁,

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
 

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],

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,