chore(topology): make topological_space fields protected (#2867)

This uses the recent `protect_proj` attribute (#2855).

src/topology/bases.lean

@@ -50,14 +50,14 @@ let b' := (λf, ⋂₀ f) '' {f:set (set α) | finite f ∧ f ⊆ s ∧ (⋂₀
   this ▸ hs⟩
 
 lemma is_topological_basis_of_open_of_nhds {s : set (set α)}
-  (h_open : ∀ u ∈ s, _root_.is_open u)
-  (h_nhds : ∀(a:α) (u : set α), a ∈ u → _root_.is_open u → ∃v ∈ s, a ∈ v ∧ v ⊆ u) :
+  (h_open : ∀ u ∈ s, is_open u)
+  (h_nhds : ∀(a:α) (u : set α), a ∈ u → is_open u → ∃v ∈ s, a ∈ v ∧ v ⊆ u) :
   is_topological_basis s :=
 ⟨assume t₁ ht₁ t₂ ht₂ x ⟨xt₁, xt₂⟩,
     h_nhds x (t₁ ∩ t₂) ⟨xt₁, xt₂⟩
-      (is_open_inter _ _ _ (h_open _ ht₁) (h_open _ ht₂)),
+      (is_open_inter (h_open _ ht₁) (h_open _ ht₂)),
   eq_univ_iff_forall.2 $ assume a,
-    let ⟨u, h₁, h₂, _⟩ := h_nhds a univ trivial (is_open_univ _) in
+    let ⟨u, h₁, h₂, _⟩ := h_nhds a univ trivial is_open_univ in
     ⟨u, h₁, h₂⟩,
   le_antisymm
     (le_generate_from h_open)
@@ -82,25 +82,25 @@ begin
 end
 
 lemma is_open_of_is_topological_basis {s : set α} {b : set (set α)}
-  (hb : is_topological_basis b) (hs : s ∈ b) : _root_.is_open s :=
+  (hb : is_topological_basis b) (hs : s ∈ b) : is_open s :=
 is_open_iff_mem_nhds.2 $ λ a as,
 (mem_nhds_of_is_topological_basis hb).2 ⟨s, hs, as, subset.refl _⟩
 
 lemma mem_basis_subset_of_mem_open {b : set (set α)}
   (hb : is_topological_basis b) {a:α} {u : set α} (au : a ∈ u)
-  (ou : _root_.is_open u) : ∃v ∈ b, a ∈ v ∧ v ⊆ u :=
+  (ou : is_open u) : ∃v ∈ b, a ∈ v ∧ v ⊆ u :=
 (mem_nhds_of_is_topological_basis hb).1 $ mem_nhds_sets ou au
 
 lemma sUnion_basis_of_is_open {B : set (set α)}
-  (hB : is_topological_basis B) {u : set α} (ou : _root_.is_open u) :
+  (hB : is_topological_basis B) {u : set α} (ou : is_open u) :
   ∃ S ⊆ B, u = ⋃₀ S :=
 ⟨{s ∈ B | s ⊆ u}, λ s h, h.1, set.ext $ λ a,
   ⟨λ ha, let ⟨b, hb, ab, bu⟩ := mem_basis_subset_of_mem_open hB ha ou in
          ⟨b, ⟨hb, bu⟩, ab⟩,
    λ ⟨b, ⟨hb, bu⟩, ab⟩, bu ab⟩⟩
 
 lemma Union_basis_of_is_open {B : set (set α)}
-  (hB : is_topological_basis B) {u : set α} (ou : _root_.is_open u) :
+  (hB : is_topological_basis B) {u : set α} (ou : is_open u) :
   ∃ (β : Type u) (f : β → set α), u = (⋃ i, f i) ∧ ∀ i, f i ∈ B :=
 let ⟨S, sb, su⟩ := sUnion_basis_of_is_open hB ou in
 ⟨S, subtype.val, su.trans set.sUnion_eq_Union, λ ⟨b, h⟩, sb h⟩
@@ -216,7 +216,7 @@ let ⟨f, hf⟩ := this in
 variables {α}
 
 lemma is_open_Union_countable [second_countable_topology α]
-  {ι} (s : ι → set α) (H : ∀ i, _root_.is_open (s i)) :
+  {ι} (s : ι → set α) (H : ∀ i, is_open (s i)) :
   ∃ T : set ι, countable T ∧ (⋃ i ∈ T, s i) = ⋃ i, s i :=
 let ⟨B, cB, _, bB⟩ := is_open_generated_countable_inter α in
 begin
@@ -231,7 +231,7 @@ begin
 end
 
 lemma is_open_sUnion_countable [second_countable_topology α]
-  (S : set (set α)) (H : ∀ s ∈ S, _root_.is_open s) :
+  (S : set (set α)) (H : ∀ s ∈ S, is_open s) :
   ∃ T : set (set α), countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
 let ⟨T, cT, hT⟩ := is_open_Union_countable (λ s:S, s.1) (λ s, H s.1 s.2) in
 ⟨subtype.val '' T, cT.image _,

src/topology/basic.lean

@@ -41,7 +41,7 @@ open_locale classical
 universes u v w
 
 /-- A topology on `α`. -/
-structure topological_space (α : Type u) :=
+@[protect_proj] structure topological_space (α : Type u) :=
 (is_open       : set α → Prop)
 (is_open_univ   : is_open univ)
 (is_open_inter  : ∀s t, is_open s → is_open t → is_open (s ∩ t))

src/topology/opens.lean

@@ -14,7 +14,7 @@ variables {α : Type*} {β : Type*} [topological_space α] [topological_space β
 namespace topological_space
 variable (α)
 /-- The type of open subsets of a topological space. -/
-def opens := {s : set α // _root_.is_open s}
+def opens := {s : set α // is_open s}
 
 /-- The type of closed subsets of a topological space. -/
 def closeds := {s : set α // is_closed s}
@@ -73,18 +73,18 @@ complete_lattice.copy
   (@galois_insertion.lift_complete_lattice
     (order_dual (set α)) (order_dual (opens α)) interior (subtype.val : opens α → set α) _ _ gi))
 /- le  -/ (λ U V, U.1 ⊆ V.1) rfl
-/- top -/ ⟨set.univ, _root_.is_open_univ⟩ (subtype.ext.mpr interior_univ.symm)
+/- top -/ ⟨set.univ, is_open_univ⟩ (subtype.ext.mpr interior_univ.symm)
 /- bot -/ ⟨∅, is_open_empty⟩ rfl
-/- sup -/ (λ U V, ⟨U.1 ∪ V.1, _root_.is_open_union U.2 V.2⟩) rfl
-/- inf -/ (λ U V, ⟨U.1 ∩ V.1, _root_.is_open_inter U.2 V.2⟩)
+/- sup -/ (λ U V, ⟨U.1 ∪ V.1, is_open_union U.2 V.2⟩) rfl
+/- inf -/ (λ U V, ⟨U.1 ∩ V.1, is_open_inter U.2 V.2⟩)
 begin
   funext,
   apply subtype.ext.mpr,
   symmetry,
   apply interior_eq_of_open,
-  exact (_root_.is_open_inter U.2 V.2),
+  exact (is_open_inter U.2 V.2),
 end
-/- Sup -/ (λ Us, ⟨⋃₀ (subtype.val '' Us), _root_.is_open_sUnion $ λ U hU,
+/- Sup -/ (λ Us, ⟨⋃₀ (subtype.val '' Us), is_open_sUnion $ λ U hU,
 by { rcases hU with ⟨⟨V, hV⟩, h, h'⟩, dsimp at h', subst h', exact hV}⟩)
 begin
   funext,

src/topology/order.lean

@@ -538,7 +538,7 @@ variables {α : Type*} {β : Type*}
 variables [t : topological_space β] {f : α → β}
 
 theorem is_open_induced_eq {s : set α} :
-  @_root_.is_open _ (induced f t) s ↔ s ∈ preimage f '' {s | is_open s} :=
+  @is_open _ (induced f t) s ↔ s ∈ preimage f '' {s | is_open s} :=
 iff.rfl
 
 theorem is_open_induced {s : set β} (h : is_open s) : (induced f t).is_open (f ⁻¹' s) :=