refactor(topology/sets/compacts): rename projection to is_compact (#1…

…6949)

In the structures `compacts`, `nonempty_compacts`, `compact_opens`, `positive_compacts` rename the field `compact` to `is_compact`.

src/measure_theory/measure/content.lean

@@ -157,9 +157,9 @@ begin
     { intros n s hn ih, rw [finset.sup_insert, finset.sum_insert hn],
       exact le_trans (μ.sup_le _ _) (add_le_add_left ih _) }},
   refine supr₂_le (λ K hK, _),
-  obtain ⟨t, ht⟩ := K.compact.elim_finite_subcover  _ (λ i, (U i).prop) _, swap,
+  obtain ⟨t, ht⟩ := K.is_compact.elim_finite_subcover  _ (λ i, (U i).prop) _, swap,
   { convert hK, rw [opens.supr_def, subtype.coe_mk] },
-  rcases K.compact.finite_compact_cover t (coe ∘ U) (λ i _, (U _).prop) (by simp only [ht])
+  rcases K.is_compact.finite_compact_cover t (coe ∘ U) (λ i _, (U _).prop) (by simp only [ht])
     with ⟨K', h1K', h2K', h3K'⟩,
   let L : ℕ → compacts G := λ n, ⟨K' n, h1K' n⟩,
   convert le_trans (h3 t L) _,

src/measure_theory/measure/haar.lean

@@ -150,8 +150,8 @@ lemma le_index_mul (K₀ : positive_compacts G) (K : compacts G) {V : set G}
   (hV : (interior V).nonempty) :
   index (K : set G) V ≤ index (K : set G) K₀ * index (K₀ : set G) V :=
 begin
-  obtain ⟨s, h1s, h2s⟩ := index_elim K.compact K₀.interior_nonempty,
-  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.compact hV,
+  obtain ⟨s, h1s, h2s⟩ := index_elim K.is_compact K₀.interior_nonempty,
+  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.is_compact hV,
   rw [← h2s, ← h2t, mul_comm],
   refine le_trans _ finset.card_mul_le,
   apply nat.Inf_le, refine ⟨_, _, rfl⟩, rw [mem_set_of_eq], refine subset.trans h1s _,
@@ -169,7 +169,7 @@ begin
   { rintro ⟨t, h1t, h2t⟩, rw [finset.card_eq_zero] at h2t, subst h2t,
     obtain ⟨g, hg⟩ := K.interior_nonempty,
     show g ∈ (∅ : set G), convert h1t (interior_subset hg), symmetry, apply bUnion_empty },
-  { exact index_defined K.compact hV }
+  { exact index_defined K.is_compact hV }
 end
 
 @[to_additive add_index_mono]
@@ -300,7 +300,7 @@ by { simp only [prehaar], rw [div_add_div_same], congr', exact_mod_cast index_un
 lemma is_left_invariant_prehaar {K₀ : positive_compacts G} {U : set G} (hU : (interior U).nonempty)
   (g : G) (K : compacts G) :
   prehaar (K₀ : set G) U (K.map _ $ continuous_mul_left g) = prehaar (K₀ : set G) U K :=
-by simp only [prehaar, compacts.coe_map, is_left_invariant_index K.compact _ hU]
+by simp only [prehaar, compacts.coe_map, is_left_invariant_index K.is_compact _ hU]
 
 /-!
 ### Lemmas about `haar_product`
@@ -540,9 +540,9 @@ end
 lemma haar_measure_self {K₀ : positive_compacts G} : haar_measure K₀ K₀ = 1 :=
 begin
   haveI : locally_compact_space G := K₀.locally_compact_space_of_group,
-  rw [haar_measure_apply K₀.compact.measurable_set, ennreal.div_self],
+  rw [haar_measure_apply K₀.is_compact.measurable_set, ennreal.div_self],
   { rw [← pos_iff_ne_zero], exact haar_content_outer_measure_self_pos },
-  { exact (content.outer_measure_lt_top_of_is_compact _ K₀.compact).ne }
+  { exact (content.outer_measure_lt_top_of_is_compact _ K₀.is_compact).ne }
 end
 
 /-- The Haar measure is regular. -/
@@ -569,7 +569,7 @@ gives  finite mass to compact sets and positive mass to nonempty open sets."]
 instance is_haar_measure_haar_measure (K₀ : positive_compacts G) :
   is_haar_measure (haar_measure K₀) :=
 begin
-  apply is_haar_measure_of_is_compact_nonempty_interior (haar_measure K₀) K₀ K₀.compact
+  apply is_haar_measure_of_is_compact_nonempty_interior (haar_measure K₀) K₀ K₀.is_compact
     K₀.interior_nonempty,
   { simp only [haar_measure_self], exact one_ne_zero },
   { simp only [haar_measure_self], exact ennreal.coe_ne_top },
@@ -593,9 +593,9 @@ left invariant measure is a scalar multiple of the additive Haar measure. This i
 than assuming that `μ` is an additive Haar measure (in particular we don't require `μ ≠ 0`)."]
 theorem haar_measure_unique (μ : measure G) [sigma_finite μ] [is_mul_left_invariant μ]
   (K₀ : positive_compacts G) : μ = μ K₀ • haar_measure K₀ :=
-(measure_eq_div_smul μ (haar_measure K₀) K₀.compact.measurable_set
+(measure_eq_div_smul μ (haar_measure K₀) K₀.is_compact.measurable_set
   (measure_pos_of_nonempty_interior _ K₀.interior_nonempty).ne'
-  K₀.compact.measure_lt_top.ne).trans (by rw [haar_measure_self, div_one])
+  K₀.is_compact.measure_lt_top.ne).trans (by rw [haar_measure_self, div_one])
 
 example [locally_compact_space G] (μ : measure G) [is_haar_measure μ] (K₀ : positive_compacts G) :
   μ = μ K₀.1 • haar_measure K₀ :=
@@ -617,11 +617,11 @@ theorem is_haar_measure_eq_smul_is_haar_measure
 begin
   have K : positive_compacts G := classical.arbitrary _,
   have νpos : 0 < ν K := measure_pos_of_nonempty_interior _ K.interior_nonempty,
-  have νne : ν K ≠ ∞ := K.compact.measure_lt_top.ne,
+  have νne : ν K ≠ ∞ := K.is_compact.measure_lt_top.ne,
   refine ⟨μ K / ν K, _, _, _⟩,
   { simp only [νne, (μ.measure_pos_of_nonempty_interior K.interior_nonempty).ne', ne.def,
       ennreal.div_zero_iff, not_false_iff, or_self] },
-  { simp only [div_eq_mul_inv, νpos.ne', (K.compact.measure_lt_top).ne, or_self,
+  { simp only [div_eq_mul_inv, νpos.ne', (K.is_compact.measure_lt_top).ne, or_self,
       ennreal.inv_eq_top, with_top.mul_eq_top_iff, ne.def, not_false_iff, and_false, false_and] },
   { calc
     μ = μ K • haar_measure K : haar_measure_unique μ K
@@ -721,7 +721,7 @@ begin
          simp, },
   have : c^2 = 1^2 :=
     (ennreal.mul_eq_mul_right (measure_pos_of_nonempty_interior _ K.interior_nonempty).ne'
-      K.compact.measure_lt_top.ne).1 this,
+      K.is_compact.measure_lt_top.ne).1 this,
   have : c = 1 := (ennreal.pow_strict_mono two_ne_zero).injective this,
   rw [hc, this, one_smul]
 end

src/measure_theory/measure/haar_lebesgue.lean

@@ -42,7 +42,7 @@ open_locale ennreal pointwise topological_space nnreal
 /-- The interval `[0,1]` as a compact set with non-empty interior. -/
 def topological_space.positive_compacts.Icc01 : positive_compacts ℝ :=
 { carrier := Icc 0 1,
-  compact' := is_compact_Icc,
+  is_compact' := is_compact_Icc,
   interior_nonempty' := by simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one] }
 
 universe u
@@ -51,7 +51,7 @@ universe u
 def topological_space.positive_compacts.pi_Icc01 (ι : Type*) [fintype ι] :
   positive_compacts (ι → ℝ) :=
 { carrier := pi univ (λ i, Icc 0 1),
-  compact' := is_compact_univ_pi (λ i, is_compact_Icc),
+  is_compact' := is_compact_univ_pi (λ i, is_compact_Icc),
   interior_nonempty' := by simp only [interior_pi_set, set.to_finite, interior_Icc,
     univ_pi_nonempty_iff, nonempty_Ioo, implies_true_iff, zero_lt_one] }
 

src/measure_theory/measure/haar_quotient.lean

@@ -156,7 +156,7 @@ begin
     h𝓕.is_mul_left_invariant_map,
   rw [measure.haar_measure_unique (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)) K,
     measure.map_apply meas_π, measure.restrict_apply₀' 𝓕meas, inter_comm],
-  exact K.compact.measurable_set,
+  exact K.is_compact.measurable_set,
 end
 
 /-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also

src/topology/algebra/group.lean

@@ -1174,7 +1174,7 @@ begin
   refine locally_compact_of_compact_nhds (λ x, _),
   obtain ⟨y, hy⟩ := K.interior_nonempty,
   let F := homeomorph.mul_left (x * y⁻¹),
-  refine ⟨F '' K, _, K.compact.image F.continuous⟩,
+  refine ⟨F '' K, _, K.is_compact.image F.continuous⟩,
   suffices : F.symm ⁻¹' K ∈ 𝓝 x, by { convert this, apply equiv.image_eq_preimage },
   apply continuous_at.preimage_mem_nhds F.symm.continuous.continuous_at,
   have : F.symm x = y, by simp [F, homeomorph.mul_left_symm],

src/topology/metric_space/baire.lean

@@ -171,7 +171,7 @@ begin
   have hK_nonempty : (⋂ n, K n : set α).nonempty,
     from is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed _
       (λ n, (hK_decreasing n).trans (inter_subset_right _ _))
-      (λ n, (K n).nonempty) (K 0).compact (λ n, (K n).compact.is_closed),
+      (λ n, (K n).nonempty) (K 0).is_compact (λ n, (K n).is_compact.is_closed),
   exact hK_nonempty.mono hK_subset
 end
 

src/topology/metric_space/closeds.lean

@@ -237,7 +237,7 @@ instance nonempty_compacts.emetric_space : emetric_space (nonempty_compacts α)
   edist_triangle      := λs t u, Hausdorff_edist_triangle,
   eq_of_edist_eq_zero := λ s t h, nonempty_compacts.ext $ begin
     have : closure (s : set α) = closure t := Hausdorff_edist_zero_iff_closure_eq_closure.1 h,
-    rwa [s.compact.is_closed.closure_eq, t.compact.is_closed.closure_eq] at this,
+    rwa [s.is_compact.is_closed.closure_eq, t.is_compact.is_closed.closure_eq] at this,
   end }
 
 /-- `nonempty_compacts.to_closeds` is a uniform embedding (as it is an isometry) -/
@@ -254,7 +254,7 @@ begin
   { ext s,
     refine ⟨_, λ h, ⟨⟨⟨s, h.2⟩, h.1⟩, closeds.ext rfl⟩⟩,
     rintro ⟨s, hs, rfl⟩,
-    exact ⟨s.nonempty, s.compact⟩ },
+    exact ⟨s.nonempty, s.is_compact⟩ },
   rw this,
   refine is_closed_of_closure_subset (λs hs, ⟨_, _⟩),
   { -- take a set set t which is nonempty and at a finite distance of s
@@ -330,7 +330,7 @@ begin
       have Fspec : ∀x, F x ∈ s ∧ edist x (F x) < δ/2 := λx, some_spec (Exy x),
 
       -- cover `t` with finitely many balls. Their centers form a set `a`
-      have : totally_bounded (t : set α) := t.compact.totally_bounded,
+      have : totally_bounded (t : set α) := t.is_compact.totally_bounded,
       rcases totally_bounded_iff.1 this (δ/2) δpos' with ⟨a, af, ta⟩,
       -- a : set α,  af : a.finite,  ta : t ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2)
       -- replace each center by a nearby approximation in `s`, giving a new set `b`
@@ -392,7 +392,7 @@ variables {α : Type u} [metric_space α]
 edistance between two such sets is finite. -/
 instance nonempty_compacts.metric_space : metric_space (nonempty_compacts α) :=
 emetric_space.to_metric_space $ λ x y, Hausdorff_edist_ne_top_of_nonempty_of_bounded
-  x.nonempty y.nonempty x.compact.bounded y.compact.bounded
+  x.nonempty y.nonempty x.is_compact.bounded y.is_compact.bounded
 
 /-- The distance on `nonempty_compacts α` is the Hausdorff distance, by construction -/
 lemma nonempty_compacts.dist_eq {x y : nonempty_compacts α} :

src/topology/metric_space/gromov_hausdorff.lean

@@ -249,7 +249,7 @@ begin
         have : Φ xX ∈ ↑p := Φrange.subst (mem_range_self _),
         exact exists_dist_lt_of_Hausdorff_dist_lt this bound
           (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty
-            p.compact.bounded q.compact.bounded) },
+            p.is_compact.bounded q.is_compact.bounded) },
       rcases this with ⟨y, hy, dy⟩,
       rcases mem_range.1 hy with ⟨z, hzy⟩,
       rw ← hzy at dy,
@@ -288,7 +288,7 @@ begin
             { apply mem_union_right, apply mem_range_self } },
           refine dist_le_diam_of_mem _ (A _) (A _),
           rw [Φrange, Ψrange],
-          exact (p ⊔ q).compact.bounded,
+          exact (p ⊔ q).is_compact.bounded,
         end
         ... ≤ 2 * diam (univ : set X) + 1 + 2 * diam (univ : set Y) : I } },
     let Fb := candidates_b_of_candidates F Fgood,
@@ -300,7 +300,7 @@ begin
       have : f (inl x) ∈ ↑p := Φrange.subst (mem_range_self _),
       rcases exists_dist_lt_of_Hausdorff_dist_lt this hr
         (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty
-          p.compact.bounded q.compact.bounded)
+          p.is_compact.bounded q.is_compact.bounded)
         with ⟨z, zq, hz⟩,
       have : z ∈ range Ψ, by rwa [← Ψrange] at zq,
       rcases mem_range.1 this with ⟨y, hy⟩,
@@ -314,7 +314,7 @@ begin
       have : f (inr y) ∈ ↑q := Ψrange.subst (mem_range_self _),
       rcases exists_dist_lt_of_Hausdorff_dist_lt' this hr
         (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty
-          p.compact.bounded q.compact.bounded)
+          p.is_compact.bounded q.is_compact.bounded)
         with ⟨z, zq, hz⟩,
       have : z ∈ range Φ, by rwa [← Φrange] at zq,
       rcases mem_range.1 this with ⟨x, hx⟩,

src/topology/metric_space/kuratowski.lean

@@ -113,5 +113,5 @@ def nonempty_compacts.Kuratowski_embedding (α : Type u) [metric_space α] [comp
   [nonempty α] :
   nonempty_compacts ℓ_infty_ℝ :=
 { carrier := range (Kuratowski_embedding α),
-  compact' := is_compact_range (Kuratowski_embedding.isometry α).continuous,
+  is_compact' := is_compact_range (Kuratowski_embedding.isometry α).continuous,
   nonempty' := range_nonempty _ }

src/topology/sets/compacts.lean

@@ -32,7 +32,7 @@ namespace topological_space
 /-- The type of compact sets of a topological space. -/
 structure compacts (α : Type*) [topological_space α] :=
 (carrier : set α)
-(compact' : is_compact carrier)
+(is_compact' : is_compact carrier)
 
 namespace compacts
 variables {α}
@@ -41,9 +41,9 @@ instance : set_like (compacts α) α :=
 { coe := compacts.carrier,
   coe_injective' := λ s t h, by { cases s, cases t, congr' } }
 
-lemma compact (s : compacts α) : is_compact (s : set α) := s.compact'
+protected lemma is_compact (s : compacts α) : is_compact (s : set α) := s.is_compact'
 
-instance (K : compacts α) : compact_space K := is_compact_iff_compact_space.1 K.compact
+instance (K : compacts α) : compact_space K := is_compact_iff_compact_space.1 K.is_compact
 
 instance : can_lift (set α) (compacts α) coe is_compact :=
 { prf := λ K hK, ⟨⟨K, hK⟩, rfl⟩ }
@@ -54,8 +54,8 @@ instance : can_lift (set α) (compacts α) coe is_compact :=
 
 @[simp] lemma carrier_eq_coe (s : compacts α) : s.carrier = s := rfl
 
-instance : has_sup (compacts α) := ⟨λ s t, ⟨s ∪ t, s.compact.union t.compact⟩⟩
-instance [t2_space α] : has_inf (compacts α) := ⟨λ s t, ⟨s ∩ t, s.compact.inter t.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 : has_bot (compacts α) := ⟨⟨∅, is_compact_empty⟩⟩
 
@@ -108,7 +108,7 @@ congr_fun (image_eq_preimage_of_inverse f.left_inv f.right_inv) K.1
 /-- The product of two `compacts`, as a `compacts` in the product space. -/
 protected def prod (K : compacts α) (L : compacts β) : compacts (α × β) :=
 { carrier := K ×ˢ L,
-  compact' := is_compact.prod K.2 L.2 }
+  is_compact' := is_compact.prod K.2 L.2 }
 
 @[simp] lemma coe_prod (K : compacts α) (L : compacts β) : (K.prod L : set (α × β)) = K ×ˢ L := rfl
 
@@ -126,11 +126,11 @@ instance : set_like (nonempty_compacts α) α :=
 { coe := λ s, s.carrier,
   coe_injective' := λ s t h, by { obtain ⟨⟨_, _⟩, _⟩ := s, obtain ⟨⟨_, _⟩, _⟩ := t, congr' } }
 
-lemma compact (s : nonempty_compacts α) : is_compact (s : set α) := s.compact'
+protected lemma is_compact (s : nonempty_compacts α) : is_compact (s : set α) := s.is_compact'
 protected lemma nonempty (s : nonempty_compacts α) : (s : set α).nonempty := s.nonempty'
 
 /-- Reinterpret a nonempty compact as a closed set. -/
-def to_closeds [t2_space α] (s : nonempty_compacts α) : closeds α := ⟨s, s.compact.is_closed⟩
+def to_closeds [t2_space α] (s : nonempty_compacts α) : closeds α := ⟨s, s.is_compact.is_closed⟩
 
 @[ext] protected lemma ext {s t : nonempty_compacts α} (h : (s : set α) = t) : s = t :=
 set_like.ext' h
@@ -156,10 +156,10 @@ order_top.lift (coe : _ → set α) (λ _ _, id) rfl
 /-- In an inhabited space, the type of nonempty compact subsets is also inhabited, with
 default element the singleton set containing the default element. -/
 instance [inhabited α] : inhabited (nonempty_compacts α) :=
-⟨{ carrier := {default}, compact' := is_compact_singleton, nonempty' := singleton_nonempty _ }⟩
+⟨{ carrier := {default}, is_compact' := is_compact_singleton, nonempty' := singleton_nonempty _ }⟩
 
 instance to_compact_space {s : nonempty_compacts α} : compact_space s :=
-is_compact_iff_compact_space.1 s.compact
+is_compact_iff_compact_space.1 s.is_compact
 
 instance to_nonempty {s : nonempty_compacts α} : nonempty s := s.nonempty.to_subtype
 
@@ -187,7 +187,7 @@ instance : set_like (positive_compacts α) α :=
 { coe := λ s, s.carrier,
   coe_injective' := λ s t h, by { obtain ⟨⟨_, _⟩, _⟩ := s, obtain ⟨⟨_, _⟩, _⟩ := t, congr' } }
 
-lemma compact (s : positive_compacts α) : is_compact (s : set α) := s.compact'
+protected lemma is_compact (s : positive_compacts α) : is_compact (s : set α) := s.is_compact'
 lemma interior_nonempty (s : positive_compacts α) : (interior (s : set α)).nonempty :=
 s.interior_nonempty'
 
@@ -252,30 +252,30 @@ end positive_compacts
 /-- The type of compact open sets of a topological space. This is useful in non Hausdorff contexts,
 in particular spectral spaces. -/
 structure compact_opens (α : Type*) [topological_space α] extends compacts α :=
-(open' : is_open carrier)
+(is_open' : is_open carrier)
 
 namespace compact_opens
 
 instance : set_like (compact_opens α) α :=
 { coe := λ s, s.carrier,
   coe_injective' := λ s t h, by { obtain ⟨⟨_, _⟩, _⟩ := s, obtain ⟨⟨_, _⟩, _⟩ := t, congr' } }
 
-lemma compact (s : compact_opens α) : is_compact (s : set α) := s.compact'
-lemma «open» (s : compact_opens α) : is_open (s : set α) := s.open'
+protected lemma is_compact (s : compact_opens α) : is_compact (s : set α) := s.is_compact'
+protected lemma is_open (s : compact_opens α) : is_open (s : set α) := s.is_open'
 
 /-- Reinterpret a compact open as an open. -/
-@[simps] def to_opens (s : compact_opens α) : opens α := ⟨s, s.open⟩
+@[simps] def to_opens (s : compact_opens α) : opens α := ⟨s, s.is_open⟩
 
 /-- Reinterpret a compact open as a clopen. -/
 @[simps] def to_clopens [t2_space α] (s : compact_opens α) : clopens α :=
-⟨s, s.open, s.compact.is_closed⟩
+⟨s, s.is_open, s.is_compact.is_closed⟩
 
 @[ext] protected lemma ext {s t : compact_opens α} (h : (s : set α) = t) : s = t := set_like.ext' h
 
 @[simp] lemma coe_mk (s : compacts α) (h) : (mk s h : set α) = s := rfl
 
 instance : has_sup (compact_opens α) :=
-⟨λ s t, ⟨s.to_compacts ⊔ t.to_compacts, s.open.union t.open⟩⟩
+⟨λ s t, ⟨s.to_compacts ⊔ t.to_compacts, s.is_open.union t.is_open⟩⟩
 
 instance [quasi_separated_space α] : has_inf (compact_opens α) :=
 ⟨λ U V, ⟨⟨(U : set α) ∩ (V : set α),
@@ -286,9 +286,9 @@ set_like.coe_injective.semilattice_inf _ (λ _ _, rfl)
 instance [compact_space α] : has_top (compact_opens α) := ⟨⟨⊤, is_open_univ⟩⟩
 instance : has_bot (compact_opens α) := ⟨⟨⊥, is_open_empty⟩⟩
 instance [t2_space α] : has_sdiff (compact_opens α) :=
-⟨λ s t, ⟨⟨s \ t, s.compact.diff t.open⟩, s.open.sdiff t.compact.is_closed⟩⟩
+⟨λ s t, ⟨⟨s \ t, s.is_compact.diff t.is_open⟩, s.is_open.sdiff t.is_compact.is_closed⟩⟩
 instance [t2_space α] [compact_space α] : has_compl (compact_opens α) :=
-⟨λ s, ⟨⟨sᶜ, s.open.is_closed_compl.is_compact⟩, s.compact.is_closed.is_open_compl⟩⟩
+⟨λ s, ⟨⟨sᶜ, s.is_open.is_closed_compl.is_compact⟩, s.is_compact.is_closed.is_open_compl⟩⟩
 
 instance : semilattice_sup (compact_opens α) :=
 set_like.coe_injective.semilattice_sup _ (λ _ _, rfl)
@@ -317,15 +317,15 @@ instance : inhabited (compact_opens α) := ⟨⊥⟩
 /-- The image of a compact open under a continuous open map. -/
 @[simps] def map (f : α → β) (hf : continuous f) (hf' : is_open_map f) (s : compact_opens α) :
   compact_opens β :=
-⟨s.to_compacts.map f hf, hf' _ s.open⟩
+⟨s.to_compacts.map f hf, hf' _ s.is_open⟩
 
 @[simp] lemma coe_map {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : compact_opens α) :
   (s.map f hf hf' : set β) = f '' s := rfl
 
 /-- The product of two `compact_opens`, as a `compact_opens` in the product space. -/
 protected def prod (K : compact_opens α) (L : compact_opens β) :
   compact_opens (α × β) :=
-{ open' := K.open.prod L.open,
+{ is_open' := K.is_open.prod L.is_open,
   .. K.to_compacts.prod L.to_compacts }
 
 @[simp] lemma coe_prod (K : compact_opens α) (L : compact_opens β) :