β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : Tendsto (fun n => EMetric.diam (A (res x n))) atTop (𝓝 0)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
hA : VanishingDiam A
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
specialize hA x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : Tendsto (fun n => EMetric.diam (A (res x n))) atTop (𝓝 0)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
rw [ENNReal.tendsto_atTop_zero] at hA
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
cases' hA (ENNReal.ofReal (ε / 2)) (by
  simp only [gt_iff_lt, ENNReal.ofReal_pos]
  linarith) with n hn
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
use n
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ dist y z < ε
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
intro y hy z hz
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ edist y z < ENNReal.ofReal ε
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ dist y z < ε
rw [← ENNReal.ofReal_lt_ofReal_iff ε_pos, ← edist_dist]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ EMetric.diam (A (res x n)) < ENNReal.ofReal ε
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ edist y z < ENNReal.ofReal ε
apply lt_of_le_of_lt (EMetric.edist_le_diam_of_mem hy hz)
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ EMetric.diam (A (res x n)) < ENNReal.ofReal ε
apply lt_of_le_of_lt (hn _ (le_refl _))
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ε / 2 < ε
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε
rw [ENNReal.ofReal_lt_ofReal_iff ε_pos]
no goals
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ε / 2 < ε
linarith
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ 0 < ε / 2
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ENNReal.ofReal (ε / 2) > 0
simp only [gt_iff_lt, ENNReal.ofReal_pos]
no goals
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ 0 < ε / 2
linarith