c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ (#↑(Iio a))
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ (#↑(Iio a)) = 𝔠
refine' le_antisymm (mk_real ▸ mk_set_le _) _
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h2 : (fun x => a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ (#↑(Iio a))
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ (#↑(Iio a))
have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by
  simp only [image_const_sub_Iio, add_sub_cancel]
no goals
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h2 : (fun x => a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ (#↑(Iio a))
exact mk_Ioi_real a ▸ h2 ▸ mk_image_le
no goals
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ (fun x => a + a - x) '' Iio a = Ioi a
simp only [image_const_sub_Iio, add_sub_cancel]