c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ (#↑(Ioi a))
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ (#↑(Ioi a)) = 𝔠
refine' le_antisymm (mk_real ▸ mk_set_le _) _
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ ¬(#↑(Ioi a)) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ (#↑(Ioi a))
rw [← not_lt]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ False
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ ¬(#↑(Ioi a)) < 𝔠
intro h
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ (#↑Set.univ) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ False
refine' _root_.ne_of_lt _ mk_univ_real
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑Set.univ) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ (#↑Set.univ) < 𝔠
have hu : Iio a ∪ {a} ∪ Ioi a = Set.univ := by
  convert @Iic_union_Ioi ℝ _ _
  exact Iio_union_right
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑(Iio a ∪ {a} ∪ Ioi a)) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑Set.univ) < 𝔠
rw [← hu]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑(Iio a ∪ {a})) + (#↑(Ioi a)) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑(Iio a ∪ {a} ∪ Ioi a)) < 𝔠
refine' lt_of_le_of_lt (mk_union_le _ _) _
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑(Iio a)) + (#↑{a}) + (#↑(Ioi a)) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑(Iio a ∪ {a})) + (#↑(Ioi a)) < 𝔠
refine' lt_of_le_of_lt (add_le_add_right (mk_union_le _ _) _) _
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑(Iio a)) + (#↑{a}) + (#↑(Ioi a)) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (#↑(Iio a)) + (#↑{a}) + (#↑(Ioi a)) < 𝔠
have h2 : (fun x => a + a - x) '' Ioi a = Iio a := by
  convert @image_const_sub_Ioi ℝ _ _ _
  simp
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑((fun x => a + a - x) '' Ioi a)) + (#↑{a}) + (#↑(Ioi a)) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑(Iio a)) + (#↑{a}) + (#↑(Ioi a)) < 𝔠
rw [← h2]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑((fun x => a + a - x) '' Ioi a)) + (#↑{a}) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑((fun x => a + a - x) '' Ioi a)) + (#↑{a}) + (#↑(Ioi a)) < 𝔠
refine' add_lt_of_lt (cantor _).le _ h
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑{a}) < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑((fun x => a + a - x) '' Ioi a)) + (#↑{a}) < 𝔠
refine' add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) _
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ (#↑{a}) < 𝔠
rw [mk_singleton]
no goals
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠
exact one_lt_aleph0.trans (cantor _)
case h.e'_2.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ Iio a ∪ {a} = Iic a
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ
convert @Iic_union_Ioi ℝ _ _
no goals
case h.e'_2.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
⊢ Iio a ∪ {a} = Iic a
exact Iio_union_right
case h.e'_3.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ a = a + a - a
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x => a + a - x) '' Ioi a = Iio a
convert @image_const_sub_Ioi ℝ _ _ _
no goals
case h.e'_3.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : (#↑(Ioi a)) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ a = a + a - a
simp