feat(data/real/cardinality): cardinalities of intervals of reals (#3252)

Use the existing result `mk_real` to deduce corresponding results for
all eight kinds of intervals of reals.

It's convenient for this result to add a new lemma to
`data.set.intervals.image_preimage` about the image of an interval
under `inv`.  Just as there are only a few results there about images
of intervals under multiplication rather than a full set, so I just
added the result I needed rather than all the possible variants.  (I
think there are something like 36 reasonable variants of that lemma
that could be stated, for (image or preimage - the same thing in this
case, but still separate statements) x (interval in positive or
negative reals) x (end closer to 0 is 0 (open), nonzero (open) or
nonzero (closed)) x (other end is open, closed or infinite).)

src/data/real/cardinality.lean

@@ -8,6 +8,7 @@ The cardinality of the reals.
 import set_theory.ordinal
 import analysis.specific_limits
 import data.rat.denumerable
+import data.set.intervals.image_preimage
 
 open nat set
 noncomputable theory
@@ -102,6 +103,7 @@ begin
     apply eq_ff_of_not_eq_tt, rw [←fn], apply ne.symm, exact nat.find_spec this }
 end
 
+/-- The cardinality of the reals, as a type. -/
 lemma mk_real : mk ℝ = 2 ^ omega.{0} :=
 begin
   apply le_antisymm,
@@ -111,7 +113,78 @@ begin
     rw [←power_def, mk_bool, mk_nat], exact 1 / 3, norm_num, norm_num }
 end
 
+/-- The cardinality of the reals, as a set. -/
+lemma mk_univ_real : mk (set.univ : set ℝ) = 2 ^ omega.{0} :=
+by rw [mk_univ, mk_real]
+
+/-- The reals are not countable. -/
 lemma not_countable_real : ¬ countable (set.univ : set ℝ) :=
-by { rw [countable_iff, not_le, mk_univ, mk_real], apply cantor }
+by { rw [countable_iff, not_le, mk_univ_real], apply cantor }
+
+/-- The cardinality of the interval (a, ∞). -/
+lemma mk_Ioi_real (a : ℝ) : mk (Ioi a) = 2 ^ omega.{0} :=
+begin
+  refine le_antisymm (mk_real ▸ mk_set_le _) _,
+  by_contradiction h,
+  rw not_le at h,
+  refine ne_of_lt _ mk_univ_real,
+  have hu : Iio a ∪ {a} ∪ Ioi a = set.univ,
+  { convert Iic_union_Ioi,
+    exact Iio_union_right },
+  rw ←hu,
+  refine lt_of_le_of_lt (mk_union_le _ _) _,
+  refine lt_of_le_of_lt (add_le_add_right _ (mk_union_le _ _)) _,
+  have h2 : (λ x, a + a - x) '' Ioi a = Iio a,
+  { convert image_const_sub_Ioi _ _,
+    simp },
+  rw ←h2,
+  refine add_lt_of_lt (le_of_lt (cantor _)) _ h,
+  refine add_lt_of_lt (le_of_lt (cantor _)) (lt_of_le_of_lt mk_image_le h) _,
+  rw mk_singleton,
+  exact lt_trans one_lt_omega (cantor _)
+end
+
+/-- The cardinality of the interval [a, ∞). -/
+lemma mk_Ici_real (a : ℝ) : mk (Ici a) = 2 ^ omega.{0} :=
+le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioi_real a ▸ mk_le_mk_of_subset Ioi_subset_Ici_self)
+
+/-- The cardinality of the interval (-∞, a). -/
+lemma mk_Iio_real (a : ℝ) : mk (Iio a) = 2 ^ omega.{0} :=
+begin
+  refine le_antisymm (mk_real ▸ mk_set_le _) _,
+  have h2 : (λ x, a + a - x) '' Iio a = Ioi a,
+  { convert image_const_sub_Iio _ _,
+    simp },
+  exact mk_Ioi_real a ▸ h2 ▸ mk_image_le
+end
+
+/-- The cardinality of the interval (-∞, a]. -/
+lemma mk_Iic_real (a : ℝ) : mk (Iic a) = 2 ^ omega.{0} :=
+le_antisymm (mk_real ▸ mk_set_le _) (mk_Iio_real a ▸ mk_le_mk_of_subset Iio_subset_Iic_self)
+
+/-- The cardinality of the interval (a, b). -/
+lemma mk_Ioo_real {a b : ℝ} (h : a < b) : mk (Ioo a b) = 2 ^ omega.{0} :=
+begin
+  refine le_antisymm (mk_real ▸ mk_set_le _) _,
+  have h1 : mk ((λ x, x - a) '' Ioo a b) ≤ mk (Ioo a b) := mk_image_le,
+  refine le_trans _ h1,
+  rw [image_sub_const_Ioo, sub_self],
+  replace h := sub_pos_of_lt h,
+  have h2 : mk (has_inv.inv '' Ioo 0 (b - a)) ≤ mk (Ioo 0 (b - a)) := mk_image_le,
+  refine le_trans _ h2,
+  rw [image_inv_Ioo_0_left h, mk_Ioi_real]
+end
+
+/-- The cardinality of the interval [a, b). -/
+lemma mk_Ico_real {a b : ℝ} (h : a < b) : mk (Ico a b) = 2 ^ omega.{0} :=
+le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ico_self)
+
+/-- The cardinality of the interval [a, b]. -/
+lemma mk_Icc_real {a b : ℝ} (h : a < b) : mk (Icc a b) = 2 ^ omega.{0} :=
+le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Icc_self)
+
+/-- The cardinality of the interval (a, b]. -/
+lemma mk_Ioc_real {a b : ℝ} (h : a < b) : mk (Ioc a b) = 2 ^ omega.{0} :=
+le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ioc_self)
 
 end cardinal

src/data/set/intervals/image_preimage.lean

@@ -12,7 +12,7 @@ import data.equiv.mul_add
 In this file we prove a bunch of trivial lemmas like “if we add `a` to all points of `[b, c]`,
 then we get `[a + b, a + c]`”. For the functions `x ↦ x ± a`, `x ↦ a ± x`, and `x ↦ -x` we prove
 lemmas about preimages and images of all intervals. We also prove a few lemmas about images under
-`x ↦ a * x` and `x ↦ x * a`.
+`x ↦ a * x`, `x ↦ x * a` and `x ↦ x⁻¹`.
 
 -/
 
@@ -285,7 +285,7 @@ by simp [sub_eq_neg_add]
 end ordered_add_comm_group
 
 /-!
-### Multiplication in a field
+### Multiplication and inverse in a field
 -/
 
 section linear_ordered_field
@@ -322,5 +322,17 @@ lemma image_mul_left_Icc {a b c : k} (ha : 0 ≤ a) (hbc : b ≤ c) :
   ((*) a) '' Icc b c = Icc (a * b) (a * c) :=
 by { convert image_mul_right_Icc hbc ha using 1; simp only [mul_comm _ a] }
 
+/-- The image under `inv` of `Ioo 0 a` is `Ioi a⁻¹`. -/
+lemma image_inv_Ioo_0_left {a : k} (ha : 0 < a) : has_inv.inv '' Ioo 0 a = Ioi a⁻¹ :=
+begin
+  ext x,
+  split,
+  { rintros ⟨y, ⟨hy0, hya⟩, hyx⟩,
+    exact hyx ▸ (inv_lt_inv ha hy0).2 hya },
+  { exact λ h, ⟨x⁻¹, ⟨inv_pos.2 (lt_trans (inv_pos.2 ha) h),
+                      (inv_lt ha (lt_trans (inv_pos.2 ha) h)).1 h⟩,
+                     inv_inv' x⟩ }
+end
+
 end linear_ordered_field
 end set

src/set_theory/cardinal.lean

@@ -927,6 +927,11 @@ theorem mk_union_add_mk_inter {α : Type u} {S T : set α} :
   mk (S ∪ T : set α) + mk (S ∩ T : set α) = mk S + mk T :=
 quot.sound ⟨equiv.set.union_sum_inter S T⟩
 
+/-- The cardinality of a union is at most the sum of the cardinalities
+of the two sets. -/
+lemma mk_union_le {α : Type u} (S T : set α) : mk (S ∪ T : set α) ≤ mk S + mk T :=
+@mk_union_add_mk_inter α S T ▸ le_add_right (mk (S ∪ T : set α)) (mk (S ∩ T : set α))
+
 theorem mk_union_of_disjoint {α : Type u} {S T : set α} (H : disjoint S T) :
   mk (S ∪ T : set α) = mk S + mk T :=
 quot.sound ⟨equiv.set.union H⟩