refactor(data/set/countable): make set.countable protected (#14886)

I'm going to add `_root_.countable` typeclass, a data-free version of `encodable`.

counterexamples/phillips.lean

@@ -212,7 +212,7 @@ def restrict (f : bounded_additive_measure α) (t : set α) : bounded_additive_m
 /-- There is a maximal countable set of positive measure, in the sense that any countable set
 not intersecting it has nonpositive measure. Auxiliary lemma to prove `exists_discrete_support`. -/
 lemma exists_discrete_support_nonpos (f : bounded_additive_measure α) :
-  ∃ (s : set α), countable s ∧ (∀ t, countable t → f (t \ s) ≤ 0) :=
+  ∃ (s : set α), s.countable ∧ (∀ t : set α, t.countable → f (t \ s) ≤ 0) :=
 begin
   /- The idea of the proof is to construct the desired set inductively, adding at each step a
   countable set with close to maximal measure among those points that have not already been chosen.
@@ -227,7 +227,7 @@ begin
   by_contra' h,
   -- We will formulate things in terms of the type of countable subsets of `α`, as this is more
   -- convenient to formalize the inductive construction.
-  let A : set (set α) := {t | countable t},
+  let A : set (set α) := {t | t.countable},
   let empty : A := ⟨∅, countable_empty⟩,
   haveI : nonempty A := ⟨empty⟩,
   -- given a countable set `s`, one can find a set `t` in its complement with measure close to
@@ -290,7 +290,7 @@ begin
 end
 
 lemma exists_discrete_support (f : bounded_additive_measure α) :
-  ∃ (s : set α), countable s ∧ (∀ t, countable t → f (t \ s) = 0) :=
+  ∃ s : set α, s.countable ∧ (∀ t : set α, t.countable → f (t \ s) = 0) :=
 begin
   rcases f.exists_discrete_support_nonpos with ⟨s₁, s₁_count, h₁⟩,
   rcases (-f).exists_discrete_support_nonpos with ⟨s₂, s₂_count, h₂⟩,
@@ -312,10 +312,10 @@ def discrete_support (f : bounded_additive_measure α) : set α :=
 (exists_discrete_support f).some
 
 lemma countable_discrete_support (f : bounded_additive_measure α) :
-  countable f.discrete_support :=
+  f.discrete_support.countable :=
 (exists_discrete_support f).some_spec.1
 
-lemma apply_countable (f : bounded_additive_measure α) (t : set α) (ht : countable t) :
+lemma apply_countable (f : bounded_additive_measure α) (t : set α) (ht : t.countable) :
   f (t \ f.discrete_support) = 0 :=
 (exists_discrete_support f).some_spec.2 t ht
 
@@ -343,7 +343,7 @@ lemma discrete_part_apply (f : bounded_additive_measure α) (s : set α) :
   f.discrete_part s = f (f.discrete_support ∩ s) := rfl
 
 lemma continuous_part_apply_eq_zero_of_countable (f : bounded_additive_measure α)
-  (s : set α) (hs : countable s) : f.continuous_part s = 0 :=
+  (s : set α) (hs : s.countable) : f.continuous_part s = 0 :=
 begin
   simp [continuous_part],
   convert f.apply_countable s hs using 2,
@@ -352,7 +352,7 @@ begin
 end
 
 lemma continuous_part_apply_diff (f : bounded_additive_measure α)
-  (s t : set α) (hs : countable s) : f.continuous_part (t \ s) = f.continuous_part t :=
+  (s t : set α) (hs : s.countable) : f.continuous_part (t \ s) = f.continuous_part t :=
 begin
   conv_rhs { rw ← diff_union_inter t s },
   rw [additive, self_eq_add_right],
@@ -449,7 +449,7 @@ We need the continuum hypothesis to construct it.
 -/
 
 theorem sierpinski_pathological_family (Hcont : #ℝ = aleph 1) :
-  ∃ (f : ℝ → set ℝ), (∀ x, countable (univ \ f x)) ∧ (∀ y, countable {x | y ∈ f x}) :=
+  ∃ (f : ℝ → set ℝ), (∀ x, (univ \ f x).countable) ∧ (∀ y, {x : ℝ | y ∈ f x}.countable) :=
 begin
   rcases cardinal.ord_eq ℝ with ⟨r, hr, H⟩,
   resetI,
@@ -477,10 +477,10 @@ contained in only countably many of them. -/
 def spf (Hcont : #ℝ = aleph 1) (x : ℝ) : set ℝ :=
 (sierpinski_pathological_family Hcont).some x
 
-lemma countable_compl_spf (Hcont : #ℝ = aleph 1) (x : ℝ) : countable (univ \ spf Hcont x) :=
+lemma countable_compl_spf (Hcont : #ℝ = aleph 1) (x : ℝ) : (univ \ spf Hcont x).countable :=
 (sierpinski_pathological_family Hcont).some_spec.1 x
 
-lemma countable_spf_mem (Hcont : #ℝ = aleph 1) (y : ℝ) : countable {x | y ∈ spf Hcont x} :=
+lemma countable_spf_mem (Hcont : #ℝ = aleph 1) (y : ℝ) : {x | y ∈ spf Hcont x}.countable :=
 (sierpinski_pathological_family Hcont).some_spec.2 y
 
 /-!
@@ -516,7 +516,7 @@ begin
 end
 
 lemma countable_ne (Hcont : #ℝ = aleph 1) (φ : (discrete_copy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
-  countable {x | φ.to_bounded_additive_measure.continuous_part univ ≠ φ (f Hcont x)} :=
+  {x | φ.to_bounded_additive_measure.continuous_part univ ≠ φ (f Hcont x)}.countable :=
 begin
   have A : {x | φ.to_bounded_additive_measure.continuous_part univ ≠ φ (f Hcont x)}
     ⊆ {x | φ.to_bounded_additive_measure.discrete_support ∩ spf Hcont x ≠ ∅},

src/analysis/box_integral/divergence_theorem.lean

@@ -140,7 +140,7 @@ TODO: If `n > 0`, then the condition at `x ∈ s` can be replaced by a much weak
 requires either better integrability theorems, or usage of a filter depending on the countable set
 `s` (we need to ensure that none of the faces of a partition contain a point from `s`). -/
 lemma has_integral_bot_pderiv (f : ℝⁿ⁺¹ → E) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E) (s : set ℝⁿ⁺¹)
-  (hs : countable s) (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
+  (hs : s.countable) (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
   (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x) (i : fin (n + 1)) :
   has_integral.{0 u u} I ⊥ (λ x, f' x (pi.single i 1)) box_additive_map.volume
     (integral.{0 u u} (I.face i) ⊥ (λ x, f (i.insert_nth (I.upper i) x)) box_additive_map.volume -
@@ -251,7 +251,7 @@ the sum of integrals of `f` over the faces of `I` taken with appropriate signs.
 More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
 we allow `f` to be non-differentiable (but still continuous) at a countable set of points. -/
 lemma has_integral_bot_divergence_of_forall_has_deriv_within_at
-  (f : ℝⁿ⁺¹ → Eⁿ⁺¹) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : countable s)
+  (f : ℝⁿ⁺¹ → Eⁿ⁺¹) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : s.countable)
   (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
   (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x) :
   has_integral.{0 u u} I ⊥ (λ x, ∑ i, f' x (pi.single i 1) i)

src/analysis/complex/cauchy_integral.lean

@@ -160,7 +160,7 @@ integral of `f` over the boundary of the rectangle is equal to the integral of
 $2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
 over the rectangle. -/
 lemma integral_boundary_rect_of_has_fderiv_at_real_off_countable (f : ℂ → E)
-  (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ) (s : set ℂ) (hs : countable s)
+  (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ) (s : set ℂ) (hs : s.countable)
   (Hc : continuous_on f ([z.re, w.re] ×ℂ [z.im, w.im]))
   (Hd : ∀ x ∈ (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im)) \ s,
     has_fderiv_at f (f' x) x)
@@ -234,7 +234,7 @@ over the boundary of a rectangle equals zero. More precisely, if `f` is continuo
 rectangle and is complex differentiable at all but countably many points of the corresponding open
 rectangle, then its integral over the boundary of the rectangle equals zero. -/
 lemma integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f : ℂ → E)
-  (z w : ℂ) (s : set ℂ) (hs : countable s) (Hc : continuous_on f ([z.re, w.re] ×ℂ [z.im, w.im]))
+  (z w : ℂ) (s : set ℂ) (hs : s.countable) (Hc : continuous_on f ([z.re, w.re] ×ℂ [z.im, w.im]))
   (Hd : ∀ x ∈ (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im)) \ s,
     differentiable_at ℂ f x) :
   (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
@@ -276,7 +276,7 @@ differentiable at all but countably many points of its interior, then the integr
 `f z / (z - c)` (formally, `(z - c)⁻¹ • f z`) over the circles `∥z - c∥ = r` and `∥z - c∥ = R` are
 equal to each other. -/
 lemma circle_integral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable
-  {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : set ℂ} (hs : countable s)
+  {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : set ℂ} (hs : s.countable)
   (hc : continuous_on f (closed_ball c R \ ball c r))
   (hd : ∀ z ∈ ball c R \ closed_ball c r \ s, differentiable_at ℂ f z) :
   ∮ z in C(c, R), (z - c)⁻¹ • f z = ∮ z in C(c, r), (z - c)⁻¹ • f z :=
@@ -296,7 +296,7 @@ begin
   set R := [a, b] ×ℂ [0, 2 * π],
   set g : ℂ → ℂ := (+) c ∘ exp,
   have hdg : differentiable ℂ g := differentiable_exp.const_add _,
-  replace hs : countable (g ⁻¹' s) := (hs.preimage (add_right_injective c)).preimage_cexp,
+  replace hs : (g ⁻¹' s).countable := (hs.preimage (add_right_injective c)).preimage_cexp,
   have h_maps : maps_to g R A,
   { rintro z ⟨h, -⟩, simpa [dist_eq, g, abs_exp, hle] using h.symm },
   replace hc : continuous_on (f ∘ g) R, from hc.comp hdg.continuous.continuous_on h_maps,
@@ -314,7 +314,7 @@ end
 its interior, then the integrals of `f` over the circles `∥z - c∥ = r` and `∥z - c∥ = R` are equal
 to each other. -/
 lemma circle_integral_eq_of_differentiable_on_annulus_off_countable
-  {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : set ℂ} (hs : countable s)
+  {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : set ℂ} (hs : s.countable)
   (hc : continuous_on f (closed_ball c R \ ball c r))
   (hd : ∀ z ∈ ball c R \ closed_ball c r \ s, differentiable_at ℂ f z) :
   ∮ z in C(c, R), f z = ∮ z in C(c, r), f z :=
@@ -331,7 +331,7 @@ punctured closed disc of radius `R`, is differentiable at all but countably many
 interior of this disc, and has a limit `y` at the center of the disc, then the integral
 $\oint_{∥z-c∥=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
 lemma circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto
-  {c : ℂ} {R : ℝ} (h0 : 0 < R) {f : ℂ → E} {y : E} {s : set ℂ} (hs : countable s)
+  {c : ℂ} {R : ℝ} (h0 : 0 < R) {f : ℂ → E} {y : E} {s : set ℂ} (hs : s.countable)
   (hc : continuous_on f (closed_ball c R \ {c}))
   (hd : ∀ z ∈ ball c R \ {c} \ s, differentiable_at ℂ f z) (hy : tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)) :
   ∮ z in C(c, R), (z - c)⁻¹ • f z = (2 * π * I : ℂ) • y :=
@@ -386,7 +386,7 @@ end
 on a closed disc of radius `R` and is complex differentiable at all but countably many points of its
 interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
 lemma circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 < R)
-  {f : ℂ → E} {c : ℂ} {s : set ℂ} (hs : countable s)
+  {f : ℂ → E} {c : ℂ} {s : set ℂ} (hs : s.countable)
   (hc : continuous_on f (closed_ball c R)) (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
   ∮ z in C(c, R), (z - c)⁻¹ • f z = (2 * π * I : ℂ) • f c :=
 circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto h0 hs
@@ -397,7 +397,7 @@ circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendst
 `{z | ∥z - c∥ ≤ R}` and is complex differentiable at all but countably many points of its interior,
 then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero. -/
 lemma circle_integral_eq_zero_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E}
-  {c : ℂ} {s : set ℂ} (hs : countable s) (hc : continuous_on f (closed_ball c R))
+  {c : ℂ} {s : set ℂ} (hs : s.countable) (hc : continuous_on f (closed_ball c R))
   (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
   ∮ z in C(c, R), f z = 0 :=
 begin
@@ -415,13 +415,13 @@ end
 `complex.circle_integral_sub_inv_smul_of_differentiable_on_off_countable`. This lemma assumes
 `w ∉ s` while the main lemma drops this assumption. -/
 lemma circle_integral_sub_inv_smul_of_differentiable_on_off_countable_aux {R : ℝ} {c w : ℂ}
-  {f : ℂ → E} {s : set ℂ} (hs : countable s) (hw : w ∈ ball c R \ s)
+  {f : ℂ → E} {s : set ℂ} (hs : s.countable) (hw : w ∈ ball c R \ s)
   (hc : continuous_on f (closed_ball c R)) (hd : ∀ x ∈ ball c R \ s, differentiable_at ℂ f x) :
   ∮ z in C(c, R), (z - w)⁻¹ • f z = (2 * π * I : ℂ) • f w :=
 begin
   have hR : 0 < R := dist_nonneg.trans_lt hw.1,
   set F : ℂ → E := dslope f w,
-  have hws : countable (insert w s) := hs.insert _,
+  have hws : (insert w s).countable := hs.insert w,
   have hnhds : closed_ball c R ∈ 𝓝 w, from closed_ball_mem_nhds_of_mem hw.1,
   have hcF : continuous_on F (closed_ball c R),
     from (continuous_on_dslope $ closed_ball_mem_nhds_of_mem hw.1).2 ⟨hc, hd _ hw⟩,
@@ -448,7 +448,7 @@ complex differentiable at all but countably many points of its interior, then fo
 interior we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
 -/
 lemma two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable
-  {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ} (hs : countable s) (hw : w ∈ ball c R)
+  {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ} (hs : s.countable) (hw : w ∈ ball c R)
   (hc : continuous_on f (closed_ball c R)) (hd : ∀ x ∈ ball c R \ s, differentiable_at ℂ f x) :
   (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z = f w :=
 begin
@@ -475,7 +475,7 @@ begin
     with ⟨l, u, hlu₀, hlu_sub⟩,
   obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).nonempty,
   { refine nonempty_diff.2 (λ hsub, _),
-    have : countable (Ioo l u),
+    have : (Ioo l u).countable,
       from (hs.preimage ((add_right_injective w).comp of_real_injective)).mono hsub,
     rw [← cardinal.mk_set_le_aleph_0, cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this,
     exact this.not_lt cardinal.aleph_0_lt_continuum },
@@ -487,7 +487,7 @@ complex differentiable at all but countably many points of its interior, then fo
 interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
 -/
 lemma circle_integral_sub_inv_smul_of_differentiable_on_off_countable
-  {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ} (hs : countable s) (hw : w ∈ ball c R)
+  {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ} (hs : s.countable) (hw : w ∈ ball c R)
   (hc : continuous_on f (closed_ball c R)) (hd : ∀ x ∈ ball c R \ s, differentiable_at ℂ f x) :
   ∮ z in C(c, R), (z - w)⁻¹ • f z = (2 * π * I : ℂ) • f w :=
 by { rw [← two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable
@@ -514,7 +514,7 @@ complex differentiable at all but countably many points of its interior, then fo
 interior we have $\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$.
 -/
 lemma circle_integral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {s : set ℂ}
-  (hs : countable s) (hw : w ∈ ball c R) {f : ℂ → ℂ} (hc : continuous_on f (closed_ball c R))
+  (hs : s.countable) (hw : w ∈ ball c R) {f : ℂ → ℂ} (hc : continuous_on f (closed_ball c R))
   (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
   ∮ z in C(c, R), f z / (z - w) = 2 * π * I * f w :=
 by simpa only [smul_eq_mul, div_eq_inv_mul]
@@ -524,7 +524,7 @@ by simpa only [smul_eq_mul, div_eq_inv_mul]
 but countably many points of the corresponding open ball, then it is analytic on the open ball with
 coefficients of the power series given by Cauchy integral formulas. -/
 lemma has_fpower_series_on_ball_of_differentiable_off_countable {R : ℝ≥0} {c : ℂ} {f : ℂ → E}
-  {s : set ℂ} (hs : countable s) (hc : continuous_on f (closed_ball c R))
+  {s : set ℂ} (hs : s.countable) (hc : continuous_on f (closed_ball c R))
   (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) (hR : 0 < R) :
   has_fpower_series_on_ball f (cauchy_power_series f c R) c R :=
 { r_le := le_radius_cauchy_power_series _ _ _,

src/analysis/special_functions/complex/log.lean

@@ -86,7 +86,7 @@ by rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
 lemma exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ n : ℤ, x = y + n * ((2 * π) * I) :=
 by simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']
 
-@[simp] lemma countable_preimage_exp {s : set ℂ} : countable (exp ⁻¹' s) ↔ countable s :=
+@[simp] lemma countable_preimage_exp {s : set ℂ} : (exp ⁻¹' s).countable ↔ s.countable :=
 begin
   refine ⟨λ hs, _, λ hs, _⟩,
   { refine ((hs.image exp).insert 0).mono _,

src/data/complex/cardinality.lean

@@ -26,5 +26,5 @@ by rw [mk_congr complex.equiv_real_prod, mk_prod, lift_id, mk_real, continuum_mu
 by rw [mk_univ, mk_complex]
 
 /-- The complex numbers are not countable. -/
-lemma not_countable_complex : ¬ countable (set.univ : set ℂ) :=
+lemma not_countable_complex : ¬ (set.univ : set ℂ).countable :=
 by { rw [← mk_set_le_aleph_0, not_le, mk_univ_complex], apply cantor }

src/data/real/cardinality.lean

@@ -163,7 +163,7 @@ lemma mk_univ_real : #(set.univ : set ℝ) = 𝔠 :=
 by rw [mk_univ, mk_real]
 
 /-- **Non-Denumerability of the Continuum**: The reals are not countable. -/
-lemma not_countable_real : ¬ countable (set.univ : set ℝ) :=
+lemma not_countable_real : ¬ (set.univ : set ℝ).countable :=
 by { rw [← mk_set_le_aleph_0, not_le, mk_univ_real], apply cantor }
 
 /-- The cardinality of the interval (a, ∞). -/