[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
⊢ BaireSpace α
[PROOFSTEP]
refine' ⟨fun f ho hd => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
⊢ Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
⊢ Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
have Bpos : ∀ n, 0 < B n := by
  intro n
  simp only [one_div, one_mul, ENNReal.inv_pos]
  exact pow_ne_top two_ne_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
⊢ ∀ (n : ℕ), 0 < B n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
n : ℕ
⊢ 0 < B n
[PROOFSTEP]
simp only [one_div, one_mul, ENNReal.inv_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
n : ℕ
⊢ 2 ^ n ≠ ⊤
[PROOFSTEP]
exact pow_ne_top two_ne_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
⊢ Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
have : ∀ n x δ, δ ≠ 0 → ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n :=
  by
  intro n x δ δpos
  have : x ∈ closure (f n) := hd n x
  rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
  rw [edist_comm] at xy 
  obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedBall y r ⊆ f n :=
    nhds_basis_closed_eball.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
  refine' ⟨y, min (min (δ / 2) r) (B (n + 1)), _, _, fun z hz => ⟨_, _⟩⟩
  show 0 < min (min (δ / 2) r) (B (n + 1))
  exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))
  show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
  exact min_le_right _ _
  show z ∈ closedBall x δ
  exact
    calc
      edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
      _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := (add_le_add hz (le_of_lt xy))
      _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
      _ = δ := ENNReal.add_halves δ
  show z ∈ f n
  exact
    hr
      (calc
        edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
        _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
⊢ ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
[PROOFSTEP]
intro n x δ δpos
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
[PROOFSTEP]
have : x ∈ closure (f n) := hd n x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
[PROOFSTEP]
rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist x y < δ / 2
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
[PROOFSTEP]
rw [edist_comm] at xy 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
[PROOFSTEP]
obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedBall y r ⊆ f n :=
  nhds_basis_closed_eball.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
[PROOFSTEP]
refine' ⟨y, min (min (δ / 2) r) (B (n + 1)), _, _, fun z hz => ⟨_, _⟩⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ 0 < min (min (δ / 2) r) (B (n + 1))
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedBall x δ
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
show 0 < min (min (δ / 2) r) (B (n + 1))
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ 0 < min (min (δ / 2) r) (B (n + 1))
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedBall x δ
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedBall x δ
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
⊢ min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedBall x δ
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
exact min_le_right _ _
[GOAL]
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedBall x δ
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
show z ∈ closedBall x δ
[GOAL]
case intro.intro.intro.intro.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedBall x δ
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
exact
  calc
    edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
    _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := (add_le_add hz (le_of_lt xy))
    _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
    _ = δ := ENNReal.add_halves δ
[GOAL]
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
show z ∈ f n
[GOAL]
case intro.intro.intro.intro.refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : α
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : α
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedBall y r ⊆ f n
z : α
hz : z ∈ closedBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n
[PROOFSTEP]
exact
  hr
    (calc
      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
this : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedBall y r ⊆ closedBall x δ ∩ f n
⊢ Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
choose! center radius Hpos HB Hball using this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
⊢ Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
refine' fun x =>
  (mem_closure_iff_nhds_basis nhds_basis_closed_eball).2 fun ε εpos =>
    _
      /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all
          `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed
          ball `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that
          `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a
          limit which belongs to all the `f n`. -/
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
let F : ℕ → α × ℝ≥0∞ := fun n =>
  Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
let c : ℕ → α := fun n => (F n).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
let r : ℕ → ℝ≥0∞ := fun n => (F n).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
have rpos : ∀ n, 0 < r n := by
  intro n
  induction' n with n hn
  exact lt_min εpos (Bpos 0)
  exact Hpos n (c n) (r n) hn.ne'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
⊢ ∀ (n : ℕ), 0 < r n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
n : ℕ
⊢ 0 < r n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
⊢ 0 < r Nat.zero
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
n : ℕ
hn : 0 < r n
⊢ 0 < r (Nat.succ n)
[PROOFSTEP]
exact lt_min εpos (Bpos 0)
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
n : ℕ
hn : 0 < r n
⊢ 0 < r (Nat.succ n)
[PROOFSTEP]
exact Hpos n (c n) (r n) hn.ne'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
have rB : ∀ n, r n ≤ B n := by
  intro n
  induction' n with n _
  exact min_le_right _ _
  exact HB n (c n) (r n) (r0 n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
⊢ ∀ (n : ℕ), r n ≤ B n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
⊢ r n ≤ B n
[PROOFSTEP]
induction' n with n _
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
⊢ r Nat.zero ≤ B Nat.zero
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
n_ih✝ : r n ≤ B n
⊢ r (Nat.succ n) ≤ B (Nat.succ n)
[PROOFSTEP]
exact min_le_right _ _
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
n_ih✝ : r n ≤ B n
⊢ r (Nat.succ n) ≤ B (Nat.succ n)
[PROOFSTEP]
exact HB n (c n) (r n) (r0 n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := fun n =>
  Hball n (c n) (r n) (r0 n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
have cdist : ∀ n, edist (c n) (c (n + 1)) ≤ B n := by
  intro n
  rw [edist_comm]
  have A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1)) := mem_closedBall_self
  have I :=
    calc
      closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) := Subset.trans (incl n) (inter_subset_left _ _)
      _ ⊆ closedBall (c n) (B n) := closedBall_subset_closedBall (rB n)
  exact I A
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
⊢ ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
n : ℕ
⊢ edist (c n) (c (n + 1)) ≤ B n
[PROOFSTEP]
rw [edist_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
n : ℕ
⊢ edist (c (n + 1)) (c n) ≤ B n
[PROOFSTEP]
have A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1)) := mem_closedBall_self
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
n : ℕ
A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1))
⊢ edist (c (n + 1)) (c n) ≤ B n
[PROOFSTEP]
have I :=
  calc
    closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) := Subset.trans (incl n) (inter_subset_left _ _)
    _ ⊆ closedBall (c n) (B n) := closedBall_subset_closedBall (rB n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
n : ℕ
A : c (n + 1) ∈ closedBall (c (n + 1)) (r (n + 1))
I : closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (B n)
⊢ edist (c (n + 1)) (c n) ≤ B n
[PROOFSTEP]
exact I A
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
have : CauchySeq c := cauchySeq_of_edist_le_geometric_two _ one_ne_top cdist
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
rcases cauchySeq_tendsto_of_complete this with
  ⟨y, ylim⟩
    -- this point `y` will be the desired point. We will check that it belongs to all
      -- `f n` and to `ball x ε`.
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
⊢ ∃ y, y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
use y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
⊢ y ∈ ⋂ (n : ℕ), f n ∧ y ∈ closedBall x ε
[PROOFSTEP]
simp only [exists_prop, Set.mem_iInter]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedBall x ε
[PROOFSTEP]
have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) :=
  by
  intro n
  refine' Nat.le_induction _ fun m _ h => _
  · exact Subset.refl _
  · exact Subset.trans (incl m) (Subset.trans (inter_subset_left _ _) h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
⊢ ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
n : ℕ
⊢ ∀ (m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
[PROOFSTEP]
refine' Nat.le_induction _ fun m _ h => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
n : ℕ
⊢ closedBall (c n) (r n) ⊆ closedBall (c n) (r n)
[PROOFSTEP]
exact Subset.refl _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
n m : ℕ
x✝ : n ≤ m
h : closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
⊢ closedBall (c (m + 1)) (r (m + 1)) ⊆ closedBall (c n) (r n)
[PROOFSTEP]
exact Subset.trans (incl m) (Subset.trans (inter_subset_left _ _) h)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedBall x ε
[PROOFSTEP]
have yball : ∀ n, y ∈ closedBall (c n) (r n) := by
  intro n
  refine' isClosed_ball.mem_of_tendsto ylim _
  refine' (Filter.eventually_ge_atTop n).mono fun m hm => _
  exact I n m hm mem_closedBall_self
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
⊢ ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
n : ℕ
⊢ y ∈ closedBall (c n) (r n)
[PROOFSTEP]
refine' isClosed_ball.mem_of_tendsto ylim _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
n : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, c x ∈ closedBall (c n) (r n)
[PROOFSTEP]
refine' (Filter.eventually_ge_atTop n).mono fun m hm => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
n m : ℕ
hm : n ≤ m
⊢ c m ∈ closedBall (c n) (r n)
[PROOFSTEP]
exact I n m hm mem_closedBall_self
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedBall x ε
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
⊢ ∀ (i : ℕ), y ∈ f i
case h.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
⊢ y ∈ closedBall x ε
[PROOFSTEP]
show ∀ n, y ∈ f n
[GOAL]
case h.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
⊢ ∀ (n : ℕ), y ∈ f n
[PROOFSTEP]
intro n
[GOAL]
case h.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
n : ℕ
⊢ y ∈ f n
[PROOFSTEP]
have : closedBall (c (n + 1)) (r (n + 1)) ⊆ f n := Subset.trans (incl n) (inter_subset_right _ _)
[GOAL]
case h.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this✝ : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
n : ℕ
this : closedBall (c (n + 1)) (r (n + 1)) ⊆ f n
⊢ y ∈ f n
[PROOFSTEP]
exact this (yball (n + 1))
[GOAL]
case h.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
⊢ y ∈ closedBall x ε
[PROOFSTEP]
show edist y x ≤ ε
[GOAL]
case h.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : CompleteSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → α → ℝ≥0∞ → α
radius : ℕ → α → ℝ≥0∞ → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : α) (δ : ℝ≥0∞), δ ≠ 0 → closedBall (center n x δ) (radius n x δ) ⊆ closedBall x δ ∩ f n
x : α
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → α × ℝ≥0∞ := fun n => Nat.recOn n (x, min ε (B 0)) fun n p => (center n p.fst p.snd, radius n p.fst p.snd)
c : ℕ → α := fun n => (F n).fst
r : ℕ → ℝ≥0∞ := fun n => (F n).snd
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : α
ylim : Tendsto c atTop (𝓝 y)
I : ∀ (n m : ℕ), m ≥ n → closedBall (c m) (r m) ⊆ closedBall (c n) (r n)
yball : ∀ (n : ℕ), y ∈ closedBall (c n) (r n)
⊢ edist y x ≤ ε
[PROOFSTEP]
exact le_trans (yball 0) (min_le_left _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
⊢ BaireSpace α
[PROOFSTEP]
constructor
[GOAL]
case baire_property
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
⊢ ∀ (f : ℕ → Set α), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
intro f ho hd
[GOAL]
case baire_property
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
⊢ Dense (⋂ (n : ℕ), f n)
[PROOFSTEP]
apply dense_iff_inter_open.2
[GOAL]
case baire_property
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
⊢ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
intro U U_open U_nonempty
[GOAL]
case baire_property
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
rcases exists_positiveCompacts_subset U_open U_nonempty with ⟨K₀, hK₀⟩
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
have : ∀ (n) (K : PositiveCompacts α), ∃ K' : PositiveCompacts α, ↑K' ⊆ f n ∩ interior K :=
  by
  refine' fun n K => exists_positiveCompacts_subset ((ho n).inter isOpen_interior) _
  rw [inter_comm]
  exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
⊢ ∀ (n : ℕ) (K : PositiveCompacts α), ∃ K', ↑K' ⊆ f n ∩ interior ↑K
[PROOFSTEP]
refine' fun n K => exists_positiveCompacts_subset ((ho n).inter isOpen_interior) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
n : ℕ
K : PositiveCompacts α
⊢ Set.Nonempty (f n ∩ interior ↑K)
[PROOFSTEP]
rw [inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
n : ℕ
K : PositiveCompacts α
⊢ Set.Nonempty (interior ↑K ∩ f n)
[PROOFSTEP]
exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
this : ∀ (n : ℕ) (K : PositiveCompacts α), ∃ K', ↑K' ⊆ f n ∩ interior ↑K
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
choose K_next hK_next using this
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
let K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
have hK_decreasing : ∀ n : ℕ, ((K (n + 1)).carrier) ⊆ (f n ∩ (K n).carrier) := fun n =>
  (hK_next n (K n)).trans <| inter_subset_inter_right _ interior_subset
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
have hK_subset : (⋂ n, (K n).carrier : Set α) ⊆ U ∩ ⋂ n, f n :=
  by
  intro x hx
  simp only [mem_iInter] at hx 
  simp only [mem_inter_iff, mem_inter] at hx ⊢
  refine' ⟨hK₀ <| hx 0, _⟩
  simp only [mem_iInter]
  exact fun n =>
    (hK_decreasing n (hx (n + 1))).1
      /- Prove that `⋂ n : ℕ, K n` is not empty, as an intersection of a decreasing sequence
          of nonempty compact subsets. -/
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
⊢ ⋂ (n : ℕ), (K n).carrier ⊆ U ∩ ⋂ (n : ℕ), f n
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
x : α
hx : x ∈ ⋂ (n : ℕ), (K n).carrier
⊢ x ∈ U ∩ ⋂ (n : ℕ), f n
[PROOFSTEP]
simp only [mem_iInter] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
x : α
hx : ∀ (i : ℕ), x ∈ (Nat.rec K₀ K_next i).toCompacts.carrier
⊢ x ∈ U ∩ ⋂ (n : ℕ), f n
[PROOFSTEP]
simp only [mem_inter_iff, mem_inter] at hx ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
x : α
hx : ∀ (i : ℕ), x ∈ (Nat.rec K₀ K_next i).toCompacts.carrier
⊢ x ∈ U ∧ x ∈ ⋂ (n : ℕ), f n
[PROOFSTEP]
refine' ⟨hK₀ <| hx 0, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
x : α
hx : ∀ (i : ℕ), x ∈ (Nat.rec K₀ K_next i).toCompacts.carrier
⊢ x ∈ ⋂ (n : ℕ), f n
[PROOFSTEP]
simp only [mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
x : α
hx : ∀ (i : ℕ), x ∈ (Nat.rec K₀ K_next i).toCompacts.carrier
⊢ ∀ (i : ℕ), x ∈ f i
[PROOFSTEP]
exact fun n =>
  (hK_decreasing n (hx (n + 1))).1
    /- Prove that `⋂ n : ℕ, K n` is not empty, as an intersection of a decreasing sequence
        of nonempty compact subsets. -/
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
hK_subset : ⋂ (n : ℕ), (K n).carrier ⊆ U ∩ ⋂ (n : ℕ), f n
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
have hK_nonempty : (⋂ n, (K n).carrier : Set α).Nonempty :=
  IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed _
    (fun n => (hK_decreasing n).trans (inter_subset_right _ _)) (fun n => (K n).nonempty) (K 0).isCompact fun n =>
    (K n).isCompact.isClosed
[GOAL]
case baire_property.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
f : ℕ → Set α
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set α
U_open : IsOpen U
U_nonempty : Set.Nonempty U
K₀ : PositiveCompacts α
hK₀ : ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts α → PositiveCompacts α
hK_next : ∀ (n : ℕ) (K : PositiveCompacts α), ↑(K_next n K) ⊆ f n ∩ interior ↑K
K : ℕ → PositiveCompacts α := fun n => Nat.recOn n K₀ K_next
hK_decreasing : ∀ (n : ℕ), (K (n + 1)).carrier ⊆ f n ∩ (K n).carrier
hK_subset : ⋂ (n : ℕ), (K n).carrier ⊆ U ∩ ⋂ (n : ℕ), f n
hK_nonempty : Set.Nonempty (⋂ (n : ℕ), (K n).carrier)
⊢ Set.Nonempty (U ∩ ⋂ (n : ℕ), f n)
[PROOFSTEP]
exact hK_nonempty.mono hK_subset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
⊢ Dense (⋂₀ S)
[PROOFSTEP]
cases' S.eq_empty_or_nonempty with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : S = ∅
⊢ Dense (⋂₀ S)
[PROOFSTEP]
simp [h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
⊢ Dense (⋂₀ S)
[PROOFSTEP]
rcases hS.exists_eq_range h with ⟨f, hf⟩
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
⊢ Dense (⋂₀ S)
[PROOFSTEP]
have F : ∀ n, f n ∈ S := fun n => by rw [hf]; exact mem_range_self _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
n : ℕ
⊢ f n ∈ S
[PROOFSTEP]
rw [hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
n : ℕ
⊢ f n ∈ range f
[PROOFSTEP]
exact mem_range_self _
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
F : ∀ (n : ℕ), f n ∈ S
⊢ Dense (⋂₀ S)
[PROOFSTEP]
rw [hf, sInter_range]
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
F : ∀ (n : ℕ), f n ∈ S
⊢ Dense (⋂ (x : ℕ), f x)
[PROOFSTEP]
exact dense_iInter_of_open_nat (fun n => ho _ (F n)) fun n => hd _ (F n)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Dense (⋂ (s : β) (_ : s ∈ S), f s)
[PROOFSTEP]
rw [← sInter_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Dense (⋂₀ ((fun s => f s) '' S))
[PROOFSTEP]
apply dense_sInter_of_open
[GOAL]
case ho
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ ∀ (s : Set α), s ∈ (fun s => f s) '' S → IsOpen s
[PROOFSTEP]
rwa [ball_image_iff]
[GOAL]
case hS
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ Set.Countable ((fun s => f s) '' S)
[PROOFSTEP]
exact hS.image _
[GOAL]
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : β → Set α
ho : ∀ (s : β), s ∈ S → IsOpen (f s)
hS : Set.Countable S
hd : ∀ (s : β), s ∈ S → Dense (f s)
⊢ ∀ (s : Set α), s ∈ (fun s => f s) '' S → Dense s
[PROOFSTEP]
rwa [ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂ (s : β), f s)
[PROOFSTEP]
rw [← sInter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂₀ range fun s => f s)
[PROOFSTEP]
apply dense_sInter_of_open
[GOAL]
case ho
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ ∀ (s : Set α), (s ∈ range fun s => f s) → IsOpen s
[PROOFSTEP]
rwa [forall_range_iff]
[GOAL]
case hS
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Set.Countable (range fun s => f s)
[PROOFSTEP]
exact countable_range _
[GOAL]
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsOpen (f s)
hd : ∀ (s : β), Dense (f s)
⊢ ∀ (s : Set α), (s ∈ range fun s => f s) → Dense s
[PROOFSTEP]
rwa [forall_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ s ∈ residual α ↔ ∃ t x, IsGδ t ∧ Dense t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ s ∈ residual α → ∃ t x, IsGδ t ∧ Dense t
[PROOFSTEP]
rw [mem_residual_iff]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ (∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) →
    ∃ t x, IsGδ t ∧ Dense t
[PROOFSTEP]
rintro ⟨S, hSo, hSd, Sct, Ss⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSd : ∀ (t : Set α), t ∈ S → Dense t
Sct : Set.Countable S
Ss : ⋂₀ S ⊆ s
⊢ ∃ t x, IsGδ t ∧ Dense t
[PROOFSTEP]
refine' ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, _⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSd : ∀ (t : Set α), t ∈ S → Dense t
Sct : Set.Countable S
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)
[PROOFSTEP]
exact dense_sInter_of_open hSo Sct hSd
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ (∃ t x, IsGδ t ∧ Dense t) → s ∈ residual α
[PROOFSTEP]
rintro ⟨t, ts, ho, hd⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual α
[PROOFSTEP]
exact mem_of_superset (residual_of_dense_Gδ ho hd) ts
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
⊢ (∀ᶠ (x : α) in residual α, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ (x : α), x ∈ t → p x
[PROOFSTEP]
convert @mem_residual _ _ _ p
[GOAL]
case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
x✝ : Set α
⊢ (IsGδ x✝ ∧ Dense x✝ ∧ ∀ (x : α), x ∈ x✝ → p x) ↔ ∃ x, IsGδ x✝ ∧ Dense x✝
[PROOFSTEP]
simp_rw [exists_prop, @and_comm ((_ : Set α) ⊆ p), and_assoc]
[GOAL]
case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
p : α → Prop
x✝ : Set α
⊢ (IsGδ x✝ ∧ Dense x✝ ∧ ∀ (x : α), x ∈ x✝ → p x) ↔ IsGδ x✝ ∧ Dense x✝ ∧ x✝ ⊆ p
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsGδ (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂ (s : β), f s)
[PROOFSTEP]
rw [← sInter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable β
f : β → Set α
ho : ∀ (s : β), IsGδ (f s)
hd : ∀ (s : β), Dense (f s)
⊢ Dense (⋂₀ range fun s => f s)
[PROOFSTEP]
exact dense_sInter_of_Gδ (forall_range_iff.2 ‹_›) (countable_range _) (forall_range_iff.2 ‹_›)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ (s : β) (h : s ∈ S), f s h)
[PROOFSTEP]
rw [biInter_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ (x : ↑S), f ↑x (_ : ↑x ∈ S))
[PROOFSTEP]
haveI := hS.toEncodable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set β
f : (x : β) → x ∈ S → Set α
ho : ∀ (s : β) (H : s ∈ S), IsGδ (f s H)
hS : Set.Countable S
hd : ∀ (s : β) (H : s ∈ S), Dense (f s H)
this : Encodable ↑S
⊢ Dense (⋂ (x : ↑S), f ↑x (_ : ↑x ∈ S))
[PROOFSTEP]
exact dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (s ∩ t)
[PROOFSTEP]
rw [inter_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ (b : Bool), bif b then s else t)
[PROOFSTEP]
apply dense_iInter_of_Gδ
[GOAL]
case ho
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), IsGδ (bif s_1 then s else t)
[PROOFSTEP]
simp [Bool.forall_bool, *]
[GOAL]
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), Dense (bif s_1 then s else t)
[PROOFSTEP]
simp [Bool.forall_bool, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
⊢ Dense (⋃ (i : ι), interior (f i))
[PROOFSTEP]
let g i := (frontier (f i))ᶜ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
⊢ Dense (⋃ (i : ι), interior (f i))
[PROOFSTEP]
have hgo : ∀ i, IsOpen (g i) := fun i => isClosed_frontier.isOpen_compl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋃ (i : ι), interior (f i))
[PROOFSTEP]
have hgd : Dense (⋂ i, g i) := by
  refine' dense_iInter_of_open hgo fun i x => _
  rw [closure_compl, interior_frontier (hc _)]
  exact id
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋂ (i : ι), g i)
[PROOFSTEP]
refine' dense_iInter_of_open hgo fun i x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : α
⊢ x ∈ closure (g i)
[PROOFSTEP]
rw [closure_compl, interior_frontier (hc _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : α
⊢ x ∈ ∅ᶜ
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
⊢ Dense (⋃ (i : ι), interior (f i))
[PROOFSTEP]
refine' (hd.inter_of_Gδ hs (isGδ_iInter_of_open fun i => (hgo i)) hgd).mono _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
⊢ s ∩ ⋂ (i : ι), g i ⊆ ⋃ (i : ι), interior (f i)
[PROOFSTEP]
rintro x ⟨hxs, hxg⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : x ∈ ⋂ (i : ι), g i
⊢ x ∈ ⋃ (i : ι), interior (f i)
[PROOFSTEP]
rw [mem_iInter] at hxg 
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ (i : ι), interior (f i)
[PROOFSTEP]
rcases mem_iUnion.1 (hU hxs) with ⟨i, hi⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ (i : ι), interior (f i)
[PROOFSTEP]
exact mem_iUnion.2 ⟨i, self_diff_frontier (f i) ▸ ⟨hi, hxg _⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
t : Set ι
s : Set α
hs : IsGδ s
hd : Dense s
ht : Set.Countable t
f : ι → Set α
hc : ∀ (i : ι), i ∈ t → IsClosed (f i)
hU : s ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
⊢ Dense (⋃ (i : ι) (_ : i ∈ t), interior (f i))
[PROOFSTEP]
haveI := ht.toEncodable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
t : Set ι
s : Set α
hs : IsGδ s
hd : Dense s
ht : Set.Countable t
f : ι → Set α
hc : ∀ (i : ι), i ∈ t → IsClosed (f i)
hU : s ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
this : Encodable ↑t
⊢ Dense (⋃ (i : ι) (_ : i ∈ t), interior (f i))
[PROOFSTEP]
simp only [biUnion_eq_iUnion, SetCoe.forall'] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
t : Set ι
s : Set α
hs : IsGδ s
hd : Dense s
ht : Set.Countable t
f : ι → Set α
this : Encodable ↑t
hc : ∀ (x : ↑t), IsClosed (f ↑x)
hU : s ⊆ ⋃ (x : ↑t), f ↑x
⊢ Dense (⋃ (x : ↑t), interior (f ↑x))
[PROOFSTEP]
exact hs.dense_iUnion_interior_of_closed hd hc hU
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
T : Set (Set α)
s : Set α
hs : IsGδ s
hd : Dense s
hc : Set.Countable T
hc' : ∀ (t : Set α), t ∈ T → IsClosed t
hU : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃ (i : Set α) (_ : i ∈ T), i
[PROOFSTEP]
rwa [← sUnion_eq_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : BaireSpace α
inst✝¹ : Nonempty α
inst✝ : Encodable β
f : β → Set α
hc : ∀ (s : β), IsClosed (f s)
hU : ⋃ (s : β), f s = univ
⊢ ∃ s, Set.Nonempty (interior (f s))
[PROOFSTEP]
simpa using (dense_iUnion_interior_of_closed hc hU).nonempty
