case intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
⊢ Bounded (range f)
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
⊢ Bounded (range f)
rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with
  ⟨s, hsf, hs1⟩
case intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
⊢ Bounded (f '' s) ∧ Bounded (f '' sᶜ)
case intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
⊢ Bounded (range f)
rw [← image_univ, ← union_compl_self s, image_union, bounded_union]
case intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
⊢ ∀ (x : α), x ∈ f '' sᶜ → ∀ (y : α), y ∈ f '' sᶜ → dist x y ≤ 1
case intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
⊢ Bounded (f '' s) ∧ Bounded (f '' sᶜ)
use (hsf.image f).bounded, 1
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1
case intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
⊢ ∀ (x : α), x ∈ f '' sᶜ → ∀ (y : α), y ∈ f '' sᶜ → dist x y ≤ 1
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.494672
ι : Type ?u.494675
inst✝ : PseudoMetricSpace α
x✝ : α
s✝ t : Set α
r : ℝ
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : Set.Finite s
hs1 : ∀ (x : β × β), x ∈ sᶜ ×ˢ sᶜ → Prod.map f f x ∈ {p | dist p.fst p.snd < 1}
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1
exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)