feat: an infinite type has a "pathological relation" (leanprover-community#37965)

In the sense that `{y | ¬ r x y}` and `{x | r x y}` are both of cardinal `< #α`.

Author: vihdzp

Counterexamples/Phillips.lean

@@ -457,27 +457,13 @@ along horizontals). Such a set cannot be measurable as it would contradict Fubin
 We need the continuum hypothesis to construct it.
 -/
 
-
+-- TODO: deprecate in favor of `Cardinal.exists_rel_mk_fibers_lt`
 theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
     ∃ f : ℝ → Set ℝ, (∀ x, (univ \ f x).Countable) ∧ ∀ y, {x : ℝ | y ∈ f x}.Countable := by
-  rcases Cardinal.exists_ord_eq ℝ with ⟨r, hr, H⟩
-  refine ⟨fun x => {y | r x y}, fun x => ?_, fun y => ?_⟩
-  · have : univ \ {y | r x y} = {y | r y x} ∪ {x} := by
-      ext y
-      simp only [true_and, mem_univ, mem_setOf_eq, mem_insert_iff, union_singleton, mem_diff]
-      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, ← Hcont]
-    exact Cardinal.card_typein_lt x H
-  · rw [← Cardinal.le_aleph0_iff_set_countable, ← Cardinal.lt_aleph_one_iff, ← Hcont]
-    exact Cardinal.card_typein_lt y H
+  obtain ⟨r, hr₁, hr₂⟩ := Cardinal.exists_rel_mk_fibers_lt ℝ
+  refine ⟨fun x ↦ setOf (r x), ?_, ?_⟩
+  · simpa [Hcont, ← Set.compl_eq_univ_diff] using hr₁
+  · simpa [Hcont] using hr₂
 
 /-- A family of sets in `ℝ` which only miss countably many points, but such that any point is
 contained in only countably many of them. -/

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -264,6 +264,12 @@ theorem add_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b
     (lt_or_ge (max a b) ℵ₀).elim (fun h => (add_lt_aleph0 h h).trans_le hc) fun h => by
       rw [add_eq_self h]; exact max_lt h1 h2
 
+theorem add_one_lt_of_lt {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a < b) : a + 1 < b :=
+  add_lt_of_lt hb ha (one_lt_aleph0.trans_le hb)
+
+theorem one_add_lt_of_lt {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a < b) : 1 + a < b :=
+  add_lt_of_lt hb (one_lt_aleph0.trans_le hb) ha
+
 theorem eq_of_add_eq_of_aleph0_le {a b c : Cardinal} (h : a + b = c) (ha : a < c) (hc : ℵ₀ ≤ c) :
     b = c := by
   apply le_antisymm
@@ -313,6 +319,15 @@ theorem add_one_eq {a : Cardinal} (ha : ℵ₀ ≤ a) : a + 1 = a :=
 theorem mk_add_one_eq {α : Type*} [Infinite α] : #α + 1 = #α :=
   add_one_eq (aleph0_le_mk α)
 
+theorem mk_Iic_lt {α : Type*} [LinearOrder α] [WellFoundedLT α] (i : α)
+    (h : ord #α = typeLT α) (hα : ℵ₀ ≤ #α) : #(Iic i) < #α := by
+  rw [← Iio_insert, mk_insert self_notMem_Iio]
+  exact add_one_lt_of_lt hα (mk_Iio_lt i h)
+
+theorem mk_Ici_lt {α : Type*} [LinearOrder α] [WellFoundedGT α] (i : α)
+    (h : ord #α = typeLT αᵒᵈ) (hα : ℵ₀ ≤ #α) : #(Ici i) < #α :=
+  mk_Iic_lt (OrderDual.toDual i) h hα
+
 protected theorem eq_of_add_eq_add_left {a b c : Cardinal} (h : a + b = a + c) (ha : a < ℵ₀) :
     b = c := by
   rcases le_or_gt ℵ₀ b with hb | hb
@@ -340,6 +355,15 @@ protected theorem eq_of_add_eq_add_right {a b c : Cardinal} (h : a + b = c + b)
 
 end add
 
+/-- Infinite types permit a relation where fewer elements than its cardinality
+are missed along all verticals and fewer elements than its cardinality are hit
+along all horizontals. -/
+theorem exists_rel_mk_fibers_lt (α : Type*) [Infinite α] :
+    ∃ r : α → α → Prop, (∀ x, #{y // ¬ r x y} < #α) ∧ (∀ y, #{x // r x y} < #α) := by
+  obtain ⟨α, _, hα⟩ := exists_ord_eq_type_lt α
+  refine ⟨LT.lt, fun x ↦ ?_, fun y ↦ mk_Iio_lt _ hα⟩
+  simpa using mk_Iic_lt _ hα (aleph0_le_mk _)
+
 /-! ### Properties of `ciSup` -/
 section ciSup
 

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -1184,6 +1184,10 @@ theorem mk_Iio_lt [LinearOrder α] [WellFoundedLT α] (i : α) (h : ord #α = ty
     #(Iio i) < #α :=
   card_typein_lt (r := LT.lt) i h
 
+theorem mk_Ioi_lt {α : Type*} [LinearOrder α] [WellFoundedGT α] (i : α) (h : ord #α = typeLT αᵒᵈ) :
+    #(Ioi i) < #α :=
+  mk_Iio_lt (OrderDual.toDual i) h
+
 @[deprecated mk_Iio_lt (since := "2026-04-12")]
 theorem mk_Iio_toType_ord_lt {c : Cardinal} (i : c.ord.ToType) : #(Iio i) < c := by
   simpa using mk_Iio_lt i