β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ CauchySeq ↑f
refine' cauchy_iff.2 ⟨by infer_instance, fun s hs => _⟩
case intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
case intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
cases' CauSeq.cauchy₂ f hε with N hN
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
exists { n | n ≥ N }.image f
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})) ∧ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s
simp only [exists_prop, mem_atTop_sets, mem_map, mem_image, ge_iff_le, mem_setOf_eq]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})

case intro.intro.intro.right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})) ∧ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
constructor
no goals
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ NeBot (map (↑f) atTop)
infer_instance
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∀ (b : ℕ), N ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
exists N
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : N ≤ b
⊢ b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∀ (b : ℕ), N ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
intro b hb
no goals
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : N ≤ b
⊢ b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
exists b
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ∈ {n | N ≤ n}
ha'2 : ↑f a' = (a, b).fst
b' : ℕ
hb'1 : b' ∈ {n | N ≤ n}
hb'2 : ↑f b' = (a, b).snd
⊢ (a, b) ∈ s
case intro.intro.intro.right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (a, b) ∈ s
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ∈ {n | N ≤ n}
ha'2 : ↑f a' = (a, b).fst
b' : ℕ
hb'1 : b' ∈ {n | N ≤ n}
hb'2 : ↑f b' = (a, b).snd
⊢ (a, b) ∈ s
dsimp at ha'1 ha'2 hb'1 hb'2
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (↑f a', ↑f b') ∈ s
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (a, b) ∈ s
rw [← ha'2, ← hb'2]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ dist (↑f a') (↑f b') < ε
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (↑f a', ↑f b') ∈ s
apply hεs
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ dist (↑f a') (↑f b') < ε
rw [dist_eq_norm]
no goals
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε
apply hN <;> assumption