feat: add a typeclass for the continuum hypothesis

Counterexamples/Phillips.lean

@@ -6,9 +6,11 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Analysis.Normed.Module.HahnBanach
+import Mathlib.Analysis.Real.Cardinality
 public import Mathlib.MeasureTheory.Integral.Bochner.Set
 public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 public import Mathlib.Topology.ContinuousMap.Bounded.Star
+public import Mathlib.SetTheory.Cardinal.ContinuumHypothesis
 
 /-!
 # A counterexample on Pettis integrability
@@ -458,7 +460,7 @@ We need the continuum hypothesis to construct it.
 -/
 
 -- TODO: deprecate in favor of `Cardinal.exists_rel_mk_fibers_lt`
-theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
+theorem sierpinski_pathological_family [ContinuumHypothesis] :
     ∃ f : ℝ → Set ℝ, (∀ x, (univ \ f x).Countable) ∧ ∀ y, {x : ℝ | y ∈ f x}.Countable := by
   obtain ⟨r, hr₁, hr₂⟩ := Cardinal.exists_rel_mk_fibers_lt ℝ
   refine ⟨fun x ↦ Set.ofPred (r x), ?_, ?_⟩
@@ -467,14 +469,14 @@ theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
 
 /-- A family of sets in `ℝ` which only miss countably many points, but such that any point is
 contained in only countably many of them. -/
-def spf (Hcont : #ℝ = ℵ₁) (x : ℝ) : Set ℝ :=
-  (sierpinski_pathological_family Hcont).choose x
+def spf [ContinuumHypothesis] (x : ℝ) : Set ℝ :=
+  sierpinski_pathological_family.choose x
 
-theorem countable_compl_spf (Hcont : #ℝ = ℵ₁) (x : ℝ) : (univ \ spf Hcont x).Countable :=
-  (sierpinski_pathological_family Hcont).choose_spec.1 x
+theorem countable_compl_spf [ContinuumHypothesis] (x : ℝ) : (univ \ spf x).Countable :=
+  sierpinski_pathological_family.choose_spec.1 x
 
-theorem countable_spf_mem (Hcont : #ℝ = ℵ₁) (y : ℝ) : {x | y ∈ spf Hcont x}.Countable :=
-  (sierpinski_pathological_family Hcont).choose_spec.2 y
+theorem countable_spf_mem [ContinuumHypothesis] (y : ℝ) : {x | y ∈ spf x}.Countable :=
+  sierpinski_pathological_family.choose_spec.2 y
 
 /-!
 ### A counterexample for the Pettis integral
@@ -493,60 +495,60 @@ which is large (it has countable complement), as in the Sierpinski pathological
 /-- A family of bounded functions `f_x` from `ℝ` (seen with the discrete topology) to `ℝ` (in fact
 taking values in `{0, 1}`), indexed by a real parameter `x`, corresponding to the characteristic
 functions of the different fibers of the Sierpinski pathological family -/
-def f (Hcont : #ℝ = ℵ₁) (x : ℝ) : DiscreteCopy ℝ →ᵇ ℝ :=
-  ofNormedAddCommGroupDiscrete (indicator (spf Hcont x) 1) 1 (norm_indicator_le_one _)
+def f [ContinuumHypothesis] (x : ℝ) : DiscreteCopy ℝ →ᵇ ℝ :=
+  ofNormedAddCommGroupDiscrete (indicator (spf x) 1) 1 (norm_indicator_le_one _)
 
 set_option backward.isDefEq.respectTransparency false in
-theorem apply_f_eq_continuousPart (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ)
-    (x : ℝ) (hx : φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x = ∅) :
-    φ (f Hcont x) = φ.toBoundedAdditiveMeasure.continuousPart univ := by
+theorem apply_f_eq_continuousPart [ContinuumHypothesis] (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ)
+    (x : ℝ) (hx : φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf x = ∅) :
+    φ (f x) = φ.toBoundedAdditiveMeasure.continuousPart univ := by
   set ψ := φ.toBoundedAdditiveMeasure
-  have : φ (f Hcont x) = ψ (spf Hcont x) := rfl
-  have U : univ = spf Hcont x ∪ univ \ spf Hcont x := by simp only [union_univ, union_sdiff_self]
+  have : φ (f x) = ψ (spf x) := rfl
+  have U : univ = spf x ∪ univ \ spf x := by simp only [union_univ, union_diff_self]
   rw [this, eq_add_parts, discretePart_apply, hx, ψ.empty, zero_add, U,
     ψ.continuousPart.additive _ _ disjoint_sdiff_self_right,
-    ψ.continuousPart_apply_eq_zero_of_countable _ (countable_compl_spf Hcont x), add_zero]
+    ψ.continuousPart_apply_eq_zero_of_countable _ (countable_compl_spf x), add_zero]
 
-theorem countable_ne (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
-    {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f Hcont x)}.Countable := by
+theorem countable_ne [ContinuumHypothesis] (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
+    {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f x)}.Countable := by
   have A :
-    {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f Hcont x)} ⊆
-      {x | (φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x).Nonempty} := by
+    {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f x)} ⊆
+      {x | (φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf x).Nonempty} := by
     intro x hx
     simp only [mem_ofPred] at *
     contrapose! hx
-    exact apply_f_eq_continuousPart Hcont φ x hx |>.symm
+    exact apply_f_eq_continuousPart φ x hx |>.symm
   have B :
-    {x | (φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x).Nonempty} ⊆
-      ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf Hcont x} := by
+    {x | (φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf x).Nonempty} ⊆
+      ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf x} := by
     intro x hx
     dsimp at hx
     simp only [exists_prop, mem_iUnion, mem_ofPred_eq]
     exact hx
   apply Countable.mono (Subset.trans A B)
-  exact Countable.biUnion (countable_discreteSupport _) fun a _ => countable_spf_mem Hcont a
+  exact Countable.biUnion (countable_discreteSupport _) fun a _ => countable_spf_mem a
 
-theorem comp_ae_eq_const (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
+theorem comp_ae_eq_const [ContinuumHypothesis] (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
     ∀ᵐ x ∂volume.restrict (Icc (0 : ℝ) 1),
-      φ.toBoundedAdditiveMeasure.continuousPart univ = φ (f Hcont x) := by
+      φ.toBoundedAdditiveMeasure.continuousPart univ = φ (f x) := by
   apply ae_restrict_of_ae
-  refine measure_mono_null ?_ ((countable_ne Hcont φ).measure_zero _)
+  refine measure_mono_null ?_ ((countable_ne φ).measure_zero _)
   intro x
   simp only [imp_self, mem_ofPred_eq, mem_compl_iff]
 
-theorem integrable_comp (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
-    IntegrableOn (fun x => φ (f Hcont x)) (Icc 0 1) := by
+theorem integrable_comp [ContinuumHypothesis] (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
+    IntegrableOn (fun x => φ (f x)) (Icc 0 1) := by
   have : IntegrableOn (fun _ => φ.toBoundedAdditiveMeasure.continuousPart univ) (Icc (0 : ℝ) 1)
       volume := by simp
-  exact Integrable.congr this (comp_ae_eq_const Hcont φ)
+  exact Integrable.congr this (comp_ae_eq_const φ)
 
-theorem integral_comp (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
-    ∫ x in Icc 0 1, φ (f Hcont x) = φ.toBoundedAdditiveMeasure.continuousPart univ := by
-  rw [← integral_congr_ae (comp_ae_eq_const Hcont φ)]
+theorem integral_comp [ContinuumHypothesis] (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
+    ∫ x in Icc 0 1, φ (f x) = φ.toBoundedAdditiveMeasure.continuousPart univ := by
+  rw [← integral_congr_ae (comp_ae_eq_const φ)]
   simp
 
 /-!
-The next few statements show that the function `f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ)` takes its
+The next few statements show that the function `f : ℝ → (DiscreteCopy ℝ →ᵇ ℝ)` takes its
 values in a complete space, is scalarly measurable, is everywhere bounded by `1`, and still has
 no Pettis integral.
 -/
@@ -555,21 +557,21 @@ no Pettis integral.
 example : CompleteSpace (DiscreteCopy ℝ →ᵇ ℝ) := by infer_instance
 
 /-- The function `f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ)` is scalarly measurable. -/
-theorem measurable_comp (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
-    Measurable fun x => φ (f Hcont x) := by
+theorem measurable_comp [ContinuumHypothesis] (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
+    Measurable fun x => φ (f x) := by
   have : Measurable fun _ : ℝ => φ.toBoundedAdditiveMeasure.continuousPart univ := measurable_const
   refine this.measurable_of_countable_ne ?_
-  exact countable_ne Hcont φ
+  exact countable_ne φ
 
 /-- The function `f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ)` is uniformly bounded by `1` in norm. -/
-theorem norm_bound (Hcont : #ℝ = ℵ₁) (x : ℝ) : ‖f Hcont x‖ ≤ 1 :=
+theorem norm_bound [ContinuumHypothesis] (x : ℝ) : ‖f x‖ ≤ 1 :=
   norm_ofNormedAddCommGroup_le _ zero_le_one (norm_indicator_le_one _)
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The function `f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ)` has no Pettis integral. -/
-theorem no_pettis_integral (Hcont : #ℝ = ℵ₁) :
+theorem no_pettis_integral [ContinuumHypothesis] :
     ¬∃ g : DiscreteCopy ℝ →ᵇ ℝ,
-        ∀ φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ, ∫ x in Icc 0 1, φ (f Hcont x) = φ g := by
+        ∀ φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ, ∫ x in Icc 0 1, φ (f x) = φ g := by
   rintro ⟨g, h⟩
   simp only [integral_comp] at h
   have : g = 0 := by

Mathlib.lean

@@ -7348,6 +7348,7 @@ public import Mathlib.SetTheory.Cardinal.Cofinality.Club
 public import Mathlib.SetTheory.Cardinal.Cofinality.Enum
 public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 public import Mathlib.SetTheory.Cardinal.Continuum
+public import Mathlib.SetTheory.Cardinal.ContinuumHypothesis
 public import Mathlib.SetTheory.Cardinal.CountableCover
 public import Mathlib.SetTheory.Cardinal.Defs
 public import Mathlib.SetTheory.Cardinal.Divisibility

Mathlib/SetTheory/Cardinal/ContinuumHypothesis.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2026 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+module
+
+public import Mathlib.Data.Real.Basic
+public import Mathlib.SetTheory.Cardinal.Continuum
+
+import Mathlib.Analysis.Real.Cardinality
+
+/-!
+# The `ContinuumHypothesis` typeclass
+
+We make this a typeclass rather than an axiom so that it is immediately obvious when a theorem
+assumes this hypothesis.
+
+In mathlib, we show consequences of the continuum hypothesis with `[ContinuumHypothesis]` in
+assumptions.
+If in downstream projects you want to assume this as an axiom, you can write
+```
+@[instance] axiom continuumHypothesis : ContinuumHypothesis
+```
+
+## Main results
+
+* `ContinuumHypothesis.iff_exists_sierpinski_pathological_partition`: Sierpiński's 1919 theorem.
+-/
+
+@[expose] public section
+
+open Cardinal
+
+/--
+If `α = ℝ`, then this shows an implication by Sierpiński (1919) about the continuum hypothesis.
+-/
+theorem Cardinal.exists_sierpinski_pathological_pred_of_card_eq_aleph_one
+    {α : Type*} (hα : #α = ℵ₁) :
+    ∃ f : α → α → Prop, (∀ x, {y | ¬ f x y}.Countable) ∧ ∀ y, {x | f x y}.Countable := by
+  open Set in
+  rcases Cardinal.exists_ord_eq α with ⟨r, hr, H⟩
+  refine ⟨r, fun x => ?_, fun y => ?_⟩
+  · have : {y | ¬r x y} = {y | r y x} ∪ {x} := by
+      ext y
+      simp only [mem_setOf_eq, mem_insert_iff, union_singleton]
+      rcases trichotomous_of r x y with (h | rfl | h)
+      · simp only [h, not_or, false_iff, not_true]
+        constructor
+        · rintro rfl; exact irrefl_of r y h
+        · exact asymm h
+      · simp only [true_or, iff_true]; exact irrefl x
+      · simp only [h, iff_true, or_true]; exact asymm h
+    rw [this]
+    apply Countable.union _ (countable_singleton _)
+    rw [← Cardinal.le_aleph0_iff_set_countable, ← Cardinal.lt_aleph_one_iff, ← hα]
+    exact Cardinal.card_typein_lt x H
+  · rw [← Cardinal.le_aleph0_iff_set_countable, ← Cardinal.lt_aleph_one_iff, ← hα]
+    exact Cardinal.card_typein_lt y H
+
+theorem Cardinal.exists_sierpinski_pathological_partition_of_card_eq_aleph_one
+    {α : Type*} (hα : #α = ℵ₁) :
+    ∃ S T : Set (α × α), IsCompl S T ∧
+      (∀ x, {y | (x, y) ∈ S}.Countable) ∧ ∀ y, {x| (x, y) ∈ T}.Countable := by
+  let ⟨f, hS, hT⟩ := exists_sierpinski_pathological_pred_of_card_eq_aleph_one hα
+  refine ⟨{p | ¬f p.1 p.2}, {p | f p.1 p.2}, isCompl_compl.symm, hS, hT⟩
+
+/-- The statement that the continuum hypothesis holds.
+
+To avoid a universe parameter, we only state that this holds in universe `0`, since it can be lifted
+to other universes with subsequent theorems.
+
+See `ContinuumHypothesis.iff_aleph0_covby_continuum` and
+`ContinuumHypothesis.iff_continuum_eq_aleph_one` for typical characterizations.
+-/
+@[mk_iff ContinuumHypothesis.iff_continuum_eq_aleph_one']
+class ContinuumHypothesis where
+  /-- See `ContinuumHypothesis.of_continuum_eq_aleph_one'` for the universe-generic version. -/
+  private of_continuum_eq_aleph_one' ::
+    /-- See `ContinuumHypothesis.continuum_eq_aleph_one` for the universe-generic version. -/
+    private continuum_eq_aleph_one' : (𝔠 : Cardinal.{0}) = ℵ₁
+
+namespace ContinuumHypothesis
+
+section basic_constructors
+
+theorem iff_continuum_eq_aleph_one.{u} : ContinuumHypothesis ↔ (𝔠 : Cardinal.{u}) = ℵ₁ := by
+  rw [iff_continuum_eq_aleph_one', ← Cardinal.lift_continuum.{u, 0}, Cardinal.lift_eq_aleph_one]
+
+@[simp]
+theorem continuum_eq_aleph_one.{u} [ContinuumHypothesis] : (𝔠 : Cardinal.{u}) = ℵ₁ :=
+  iff_continuum_eq_aleph_one.1 ‹_›
+
+alias ⟨_, of_continuum_eq_aleph_one⟩ := iff_continuum_eq_aleph_one
+
+theorem iff_aleph0_covby_continuum.{u} : ContinuumHypothesis ↔ ℵ₀ ⋖ (𝔠 : Cardinal.{u}) := by
+  rw [← Order.succ_eq_iff_covBy, Cardinal.succ_aleph0, eq_comm, iff_continuum_eq_aleph_one]
+
+theorem aleph0_covby_continuum.{u} [ContinuumHypothesis] : ℵ₀ ⋖ (𝔠 : Cardinal.{u}) :=
+  iff_aleph0_covby_continuum.1 ‹_›
+
+alias ⟨_, of_aleph0_covby_continuum⟩ := iff_aleph0_covby_continuum
+
+end basic_constructors
+
+/--
+Alternate statement of `iff_exists_sierpinski_pathological_partition` using a predicate to assign
+points to sets.
+-/
+theorem iff_exists_sierpinski_pathological_pred :
+    ContinuumHypothesis ↔
+      ∃ f : ℝ → ℝ → Prop, (∀ x, {y | ¬ f x y}.Countable) ∧ ∀ y, {x : ℝ | f x y}.Countable := by
+  refine ⟨fun _ => Cardinal.exists_sierpinski_pathological_pred_of_card_eq_aleph_one ?_,
+      fun ⟨f, hnf, hf⟩ => ?_⟩
+  · simp only [Cardinal.mk_real, continuum_eq_aleph_one]
+  suffices #ℝ ≤ ℵ₁ by
+    rw [iff_continuum_eq_aleph_one]
+    apply le_antisymm (Cardinal.mk_real.symm.trans_le this)
+    exact Cardinal.aleph_one_le_continuum
+  by_contra! h_c_gt
+  obtain ⟨S, hS_card : #S = ℵ₁⟩ := Cardinal.le_mk_iff_exists_set.mp h_c_gt.le
+  haveI : Nonempty S := by
+    rw [Set.nonempty_coe_sort, ← Cardinal.mk_set_ne_zero_iff, hS_card]
+    exact (Cardinal.aleph_pos _).ne'
+  let C := ⋃ x ∈ S, {y | ¬ f x y}
+  have hC_le : #C ≤ ℵ₁ := by
+    calc #C ≤ #S * ℵ₀ := by
+            grw [Cardinal.mk_biUnion_le _ _]
+            gcongr
+            refine ciSup_le fun x => ?_
+            grw [Cardinal.le_aleph0_iff_set_countable.2 (hnf _)]
+         _ = ℵ₁ * ℵ₀ := by rw [hS_card]
+         _ = ℵ₁      := Cardinal.aleph_mul_aleph0 1
+  obtain ⟨y', hy_notin : y' ∉ C⟩ := Cardinal.compl_nonempty_of_mk_lt_mk (hC_le.trans_lt h_c_gt)
+  have h_sub : S ⊆ {x | f x y'} := by simpa [C] using hy_notin
+  have h_S_count : S.Countable := (hf y').mono h_sub
+  rw [← Cardinal.le_aleph0_iff_set_countable, hS_card] at h_S_count
+  exact h_S_count.not_gt Cardinal.aleph0_lt_aleph_one
+
+/--
+The continuum hypothesis is equivalent to the statement that
+the plane $\mathbb{R}^2$ can be partitioned into two sets,
+$A$ and $B$, such that every horizontal line intersects $A$ in a countable number of points,
+and every vertical line intersects $B$ in a countable number of points.
+
+This is Sierpiński (1919).
+-/
+theorem iff_exists_sierpinski_pathological_partition :
+    ContinuumHypothesis ↔
+      ∃ S T : Set (ℝ × ℝ), IsCompl S T ∧
+        (∀ x, {y | (x, y) ∈ S}.Countable) ∧ ∀ y, {x : ℝ | (x, y) ∈ T}.Countable := by
+  refine ⟨fun _ => exists_sierpinski_pathological_partition_of_card_eq_aleph_one ?_, ?_⟩
+  · simp only [Cardinal.mk_real, continuum_eq_aleph_one]
+  rw [iff_exists_sierpinski_pathological_pred]
+  rintro ⟨S, T, hST, hS, hT⟩
+  obtain rfl := hST.eq_compl
+  refine ⟨fun x y => (x, y) ∈ T, hS, hT⟩
+
+end ContinuumHypothesis

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -633,6 +633,7 @@ def overrideAllowedImportDirs : NamePrefixRel := .ofArray #[
   (`Mathlib.Analysis.Convex.SimplicialComplex.Basic, `Mathlib.AlgebraicTopology),
   (`Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion, `Mathlib.AlgebraicTopology),
   (`Mathlib.Probability.Kernel.Category, `Mathlib.CategoryTheory), -- For the category of s-finite/Markov kernels
+  (`Mathlib.SetTheory.Cardinal.ContinuumHypothesis, `Mathlib.Analysis.Real.Cardinality),
   (`Mathlib.RepresentationTheory.Continuous, `Mathlib.Topology), -- For continuous representations
   (`Mathlib.RepresentationTheory.Homological.ContCohomology, `Mathlib.Topology),  -- For continuous cohomology
   -- TODO: think about the role of Analysis and Algebra, and perhaps further separation