refactor(topology/basic): use dot notation in is_open.union and friends (#7647)

The fact that the union of two open sets is open is called `is_open_union`. We rename it to `is_open.union` to enable dot notation. Same with `is_open_inter`, `is_closed_union` and `is_closed_inter` and `is_clopen_union` and `is_clopen_inter` and `is_clopen_diff`.

Author: sgouezel

src/analysis/calculus/extend_deriv.lean

@@ -69,7 +69,7 @@ begin
     have bound : ∀ z ∈ (B ∩ s), ∥fderiv_within ℝ f (B ∩ s) z - f'∥ ≤ ε,
     { intros z z_in,
       convert le_of_lt (hδ _ z_in.2 z_in.1),
-      have op : is_open (B ∩ s) := is_open_inter is_open_ball s_open,
+      have op : is_open (B ∩ s) := is_open_ball.inter s_open,
       rw differentiable_at.fderiv_within _ (op.unique_diff_on z z_in),
       exact (diff z z_in).differentiable_at (mem_nhds_sets op z_in) },
     simpa using conv.norm_image_sub_le_of_norm_fderiv_within_le' diff bound u_in v_in },

src/analysis/calculus/fderiv_measurable.lean

@@ -124,7 +124,7 @@ begin
 end
 
 lemma is_open_B {K : set (E →L[𝕜] F)} {r s ε : ℝ} : is_open (B f K r s ε) :=
-by simp [B, is_open_Union, is_open_inter, is_open_A]
+by simp [B, is_open_Union, is_open.inter, is_open_A]
 
 lemma A_mono (L : E →L[𝕜] F) (r : ℝ) {ε δ : ℝ} (h : ε ≤ δ) :
   A f L r ε ⊆ A f L r δ :=

src/analysis/convex/topology.lean

@@ -60,7 +60,7 @@ lemma bounded_std_simplex : metric.bounded (std_simplex ι) :=
 
 /-- `std_simplex ι` is closed. -/
 lemma is_closed_std_simplex : is_closed (std_simplex ι) :=
-(std_simplex_eq_inter ι).symm ▸ is_closed_inter
+(std_simplex_eq_inter ι).symm ▸ is_closed.inter
   (is_closed_Inter $ λ i, is_closed_le continuous_const (continuous_apply i))
   (is_closed_eq (continuous_finset_sum _ $ λ x _, continuous_apply x) continuous_const)
 

src/data/analysis/topology.lean

@@ -126,7 +126,7 @@ protected def id : realizer α := ⟨{x:set α // is_open x},
 { f            := subtype.val,
   top          := λ _, ⟨univ, is_open_univ⟩,
   top_mem      := mem_univ,
-  inter        := λ ⟨x, h₁⟩ ⟨y, h₂⟩ a h₃, ⟨_, is_open_inter h₁ h₂⟩,
+  inter        := λ ⟨x, h₁⟩ ⟨y, h₂⟩ a h₃, ⟨_, h₁.inter h₂⟩,
   inter_mem    := λ ⟨x, h₁⟩ ⟨y, h₂⟩ a, id,
   inter_sub    := λ ⟨x, h₁⟩ ⟨y, h₂⟩ a h₃, subset.refl _ },
 ext subtype.property $ λ x s h,

src/geometry/manifold/bump_function.lean

@@ -234,7 +234,7 @@ begin
   rw f.image_eq_inter_preimage_of_subset_support hs,
   refine continuous_on.preimage_closed_of_closed
     ((ext_chart_continuous_on_symm _ _).mono f.closed_ball_subset) _ hsc,
-  exact is_closed_inter is_closed_closed_ball I.closed_range
+  exact is_closed.inter is_closed_closed_ball I.closed_range
 end
 
 /-- If `f` is a smooth bump function and `s` closed subset of the support of `f` (i.e., of the open
@@ -406,7 +406,7 @@ instance : has_coe_to_fun (smooth_bump_covering I s) := ⟨_, to_fun⟩
   (h₁ h₂ h₃) : ⇑(mk ι c to_fun h₁ h₂ h₃ : smooth_bump_covering I s) = to_fun :=
 rfl
 
-/-- 
+/--
 We say that `f : smooth_bump_covering I s` is *subordinate* to a map `U : M → set M` if for each
 index `i`, we have `closure (support (f i)) ⊆ U (f i).c`. This notion is a bit more general than
 being subordinate to an open covering of `M`, because we make no assumption about the way `U x`

src/geometry/manifold/charted_space.lean

@@ -382,7 +382,7 @@ def id_restr_groupoid : structure_groupoid H :=
 { members := {e | ∃ {s : set H} (h : is_open s), e ≈ local_homeomorph.of_set s h},
   trans' := begin
     rintros e e' ⟨s, hs, hse⟩ ⟨s', hs', hse'⟩,
-    refine ⟨s ∩ s', is_open_inter hs hs', _⟩,
+    refine ⟨s ∩ s', is_open.inter hs hs', _⟩,
     have := local_homeomorph.eq_on_source.trans' hse hse',
     rwa local_homeomorph.of_set_trans_of_set at this,
   end,
@@ -417,7 +417,7 @@ instance closed_under_restriction_id_restr_groupoid :
   closed_under_restriction (@id_restr_groupoid H _) :=
 ⟨ begin
     rintros e ⟨s', hs', he⟩ s hs,
-    use [s' ∩ s, is_open_inter hs' hs],
+    use [s' ∩ s, is_open.inter hs' hs],
     refine setoid.trans (local_homeomorph.eq_on_source.restr he s) _,
     exact ⟨by simp only [hs.interior_eq] with mfld_simps, by simp only with mfld_simps⟩,
   end ⟩

src/geometry/manifold/local_invariant_properties.lean

@@ -140,10 +140,10 @@ begin
     ∃ (o : set M), is_open o ∧ x ∈ o ∧ o ⊆ e.source ∧ o ⊆ e'.source ∧
       o ∩ s ⊆ g ⁻¹' f.source ∧ o ∩ s ⊆  g⁻¹' f'.to_local_equiv.source,
   { have : f.source ∩ f'.source ∈ 𝓝 (g x) :=
-      mem_nhds_sets (is_open_inter f.open_source f'.open_source) ⟨xf, xf'⟩,
+      mem_nhds_sets (is_open.inter f.open_source f'.open_source) ⟨xf, xf'⟩,
     rcases mem_nhds_within.1 (hgs.preimage_mem_nhds_within this) with ⟨u, u_open, xu, hu⟩,
     refine ⟨u ∩ e.source ∩ e'.source, _, ⟨⟨xu, xe⟩, xe'⟩, _, _, _, _⟩,
-    { exact is_open_inter (is_open_inter u_open e.open_source) e'.open_source },
+    { exact is_open.inter (is_open.inter u_open e.open_source) e'.open_source },
     { assume x hx, exact hx.1.2 },
     { assume x hx, exact hx.2 },
     { assume x hx, exact (hu ⟨hx.1.1.1, hx.2⟩).1 },
@@ -199,7 +199,7 @@ begin
       simp only [this, hy] with mfld_simps } },
   rw this at E,
   apply (hG.is_local _ _).2 E,
-  { exact is_open_inter w.open_target
+  { exact is_open.inter w.open_target
       (e'.continuous_on_symm.preimage_open_of_open e'.open_target o_open) },
   { simp only [xe', xe, xo] with mfld_simps },
 end
@@ -245,7 +245,7 @@ begin
       mem_nhds_sets ((chart_at H' (g x))).open_source (mem_chart_source H' (g x)),
     rcases mem_nhds_within.1 (hcont.preimage_mem_nhds_within this) with ⟨v, v_open, xv, hv⟩,
     refine ⟨u ∩ v ∩ (chart_at H x).source, _, ⟨⟨xu, xv⟩, mem_chart_source _ _⟩, _, _, _⟩,
-    { exact is_open_inter (is_open_inter u_open v_open) (chart_at H x).open_source },
+    { exact is_open.inter (is_open.inter u_open v_open) (chart_at H x).open_source },
     { assume y hy, exact hy.2 },
     { assume y hy, exact hv ⟨hy.1.1.2, hy.2⟩ },
     { assume y hy, exact ust ⟨hy.1.1.1, hy.2⟩ } },

src/geometry/manifold/times_cont_mdiff.lean

@@ -634,7 +634,7 @@ begin
         mem_nhds_sets (local_homeomorph.open_source _) (mem_chart_source H' (f x)),
       rcases mem_nhds_within.1 (h.1.preimage_mem_nhds_within this) with ⟨u, u_open, xu, hu⟩,
       refine ⟨u ∩ (chart_at H x).source, _, ⟨xu, mem_chart_source _ _⟩, _, _⟩,
-      { exact is_open_inter u_open (local_homeomorph.open_source _) },
+      { exact is_open.inter u_open (local_homeomorph.open_source _) },
       { assume y hy, exact hy.2 },
       { assume y hy, exact hu ⟨hy.1.1, hy.2⟩ } },
     have h' : times_cont_mdiff_within_at I I' n f (s ∩ o) x := h.mono (inter_subset_left _ _),
@@ -1181,7 +1181,7 @@ begin
   suffices h : times_cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) s'_lift,
   { refine ⟨(tangent_bundle.proj I M)⁻¹' (o ∩ l.source), _, _, _⟩,
     show is_open ((tangent_bundle.proj I M)⁻¹' (o ∩ l.source)), from
-      (is_open_inter o_open l.open_source).preimage (tangent_bundle_proj_continuous _ _) ,
+      (is_open.inter o_open l.open_source).preimage (tangent_bundle_proj_continuous _ _) ,
     show p ∈ tangent_bundle.proj I M ⁻¹' (o ∩ l.source),
     { simp [tangent_bundle.proj] at ⊢,
       have : p.1 ∈ f ⁻¹' r.source ∩ s, by simp [hp],

src/measure_theory/borel_space.lean

@@ -92,7 +92,7 @@ lemma topological_space.is_topological_basis.borel_eq_generate_from [topological
 borel_eq_generate_from_of_subbasis hs.eq_generate_from
 
 lemma is_pi_system_is_open [topological_space α] : is_pi_system (is_open : set α → Prop) :=
-λ s t hs ht hst, is_open_inter hs ht
+λ s t hs ht hst, is_open.inter hs ht
 
 lemma borel_eq_generate_from_is_closed [topological_space α] :
   borel α = generate_from {s | is_closed s} :=

src/measure_theory/content.lean

@@ -319,14 +319,14 @@ begin
   intros U hU,
   rw μ.outer_measure_caratheodory,
   intro U',
-  rw μ.outer_measure_of_is_open ((U' : set G) ∩ U) (is_open_inter U'.prop hU),
+  rw μ.outer_measure_of_is_open ((U' : set G) ∩ U) (is_open.inter U'.prop hU),
   simp only [inner_content, supr_subtype'], rw [opens.coe_mk],
   haveI : nonempty {L : compacts G // L.1 ⊆ U' ∩ U} := ⟨⟨⊥, empty_subset _⟩⟩,
   rw [ennreal.supr_add],
   refine supr_le _, rintro ⟨L, hL⟩, simp only [subset_inter_iff] at hL,
   have : ↑U' \ U ⊆ U' \ L.1 := diff_subset_diff_right hL.2,
   refine le_trans (add_le_add_left (μ.outer_measure.mono' this) _) _,
-  rw μ.outer_measure_of_is_open (↑U' \ L.1) (is_open_diff U'.2 L.2.is_closed),
+  rw μ.outer_measure_of_is_open (↑U' \ L.1) (is_open.sdiff U'.2 L.2.is_closed),
   simp only [inner_content, supr_subtype'], rw [opens.coe_mk],
   haveI : nonempty {M : compacts G // M.1 ⊆ ↑U' \ L.1} := ⟨⟨⊥, empty_subset _⟩⟩,
   rw [ennreal.add_supr], refine supr_le _, rintro ⟨M, hM⟩, simp only [subset_diff] at hM,