α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
let u N := (h N).some
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
have I : ∀ n N, n ≤ N → u N ∈ s n := by
  intro n N hn
  apply mem_of_subset_of_mem _ (h N).choose_spec
  intro x hx
  simp only [mem_iInter] at hx
  exact hx n hn
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
have : CauchySeq u := by
  apply cauchySeq_of_le_tendsto_0 _ _ h'
  intro m n N hm hn
  exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)
case intro.intro
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
obtain ⟨x, -, xlim⟩ : ∃ x ∈ s 0, Tendsto (fun n : ℕ => u n) atTop (𝓝 x) :=
  cauchySeq_tendsto_of_isComplete h0 (fun n => I 0 n (zero_le _)) this
case intro.intro
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n : ℕ
⊢ x ∈ s n
case intro.intro
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
⊢ Set.Nonempty (⋂ (n : ℕ), s n)
refine' ⟨x, mem_iInter.2 fun n => _⟩
case intro.intro
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, u x ∈ s n
case intro.intro
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n : ℕ
⊢ x ∈ s n
apply (hs n).mem_of_tendsto xlim
case h
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n p : ℕ
hp : p ∈ Ici n
⊢ Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ p), s n)) ∈ s n
case intro.intro
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, u x ∈ s n
filter_upwards [Ici_mem_atTop n]with p hp
no goals
case h
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun n => u n) atTop (𝓝 x)
n p : ℕ
hp : p ∈ Ici n
⊢ Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ p), s n)) ∈ s n
exact I n p hp
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
⊢ u N ∈ s n
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
⊢ ∀ (n N : ℕ), n ≤ N → u N ∈ s n
intro n N hn
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
⊢ (⋂ (n : ℕ) (_ : n ≤ N), s n) ⊆ s n
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
⊢ u N ∈ s n
apply mem_of_subset_of_mem _ (h N).choose_spec
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
x : α
hx : x ∈ ⋂ (n : ℕ) (_ : n ≤ N), s n
⊢ x ∈ s n
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
⊢ (⋂ (n : ℕ) (_ : n ≤ N), s n) ⊆ s n
intro x hx
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
x : α
hx : ∀ (i : ℕ), i ≤ N → x ∈ s i
⊢ x ∈ s n
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
x : α
hx : x ∈ ⋂ (n : ℕ) (_ : n ≤ N), s n
⊢ x ∈ s n
simp only [mem_iInter] at hx
no goals
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x✝ y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
n N : ℕ
hn : n ≤ N
x : α
hx : ∀ (i : ℕ), i ≤ N → x ∈ s i
⊢ x ∈ s n
exact hx n hn
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ diam (s N)
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ CauchySeq u
apply cauchySeq_of_le_tendsto_0 _ _ h'
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
m n N : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ dist (u m) (u n) ≤ diam (s N)
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ diam (s N)
intro m n N hm hn
no goals
α : Type u
β : Type v
X : Type ?u.540098
ι : Type ?u.540101
inst✝ : PseudoMetricSpace α
s✝ : Set α
x y z : α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed (s n)
h's : ∀ (n : ℕ), Bounded (s n)
h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)
h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N => Set.Nonempty.some (_ : Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n))
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
m n N : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ dist (u m) (u n) ≤ diam (s N)
exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)