α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ t, t ⊆ range s ∧ Set.Finite t ∧ range s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ a}
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
⊢ TotallyBounded (range s)
refine' totallyBounded_iff_subset.2 fun a ha => _
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
⊢ ∃ t, t ⊆ range s ∧ Set.Finite t ∧ range s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ a}
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ t, t ⊆ range s ∧ Set.Finite t ∧ range s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ a}
cases' cauchySeq_iff.1 hs a ha with n hn
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
⊢ range s ⊆ ⋃ (y : α) (_ : y ∈ s '' {k | k ≤ n}), {x | (x, y) ∈ a}
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
⊢ ∃ t, t ⊆ range s ∧ Set.Finite t ∧ range s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ a}
refine' ⟨s '' { k | k ≤ n }, image_subset_range _ _, (finite_le_nat _).image _, _⟩
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ (y : ℕ) (_ : y ∈ {k | k ≤ n}), {x | (x, s y) ∈ a}
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
⊢ range s ⊆ ⋃ (y : α) (_ : y ∈ s '' {k | k ≤ n}), {x | (x, y) ∈ a}
rw [range_subset_iff, biUnion_image]
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
⊢ s m ∈ ⋃ (y : ℕ) (_ : y ∈ {k | k ≤ n}), {x | (x, s y) ∈ a}
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
⊢ ∀ (y : ℕ), s y ∈ ⋃ (y : ℕ) (_ : y ∈ {k | k ≤ n}), {x | (x, s y) ∈ a}
intro m
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
⊢ ∃ i j, s m ∈ {x | (x, s i) ∈ a}
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
⊢ s m ∈ ⋃ (y : ℕ) (_ : y ∈ {k | k ≤ n}), {x | (x, s y) ∈ a}
rw [mem_iUnion₂]
case intro.inl
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
hm : m ≤ n
⊢ ∃ i j, s m ∈ {x | (x, s i) ∈ a}

case intro.inr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
hm : n ≤ m
⊢ ∃ i j, s m ∈ {x | (x, s i) ∈ a}
case intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
⊢ ∃ i j, s m ∈ {x | (x, s i) ∈ a}
cases' le_total m n with hm hm
no goals
case intro.inl
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
hm : m ≤ n
⊢ ∃ i j, s m ∈ {x | (x, s i) ∈ a}

case intro.inr
α : Type u
β : Type v
inst✝ : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ (k : ℕ), k ≥ n → ∀ (l : ℕ), l ≥ n → (s k, s l) ∈ a
m : ℕ
hm : n ≤ m
⊢ ∃ i j, s m ∈ {x | (x, s i) ∈ a}
exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]