Convergent implies bounded

Stream: Is there code for X?

[Heather Macbeth]

Can't seem to find this in the library -- do we have it? I would take either a form for orders,

example {ι : Type*} {α : Type*} [linear_order α] [topological_space α] [order_topology α]
  {f : ι → α} (a : α) (hf : tendsto f cofinite (𝓝 a)) :
  bdd_above (set.range f) :=

or for metric spaces,

example {ι : Type*} {α : Type*} [metric_space α] {f : ι → α} (a : α)
  (hf : tendsto f cofinite (𝓝 a)) : metric.bounded (set.range f) :=

[Heather Macbeth]

Maybe this breaks into two lemmas: (1) convergent implies eventually bounded; (2) for filter.cofinite, eventually bounded implies bounded.

[Heather Macbeth]

(I have messy proofs which I'll PR if nothing elegant is available.)

[Yury G. Kudryashov]

We have docs#cauchy_seq_bdd

[Yury G. Kudryashov]

It comes before the definition of metric.bounded

[Heather Macbeth]

That is for domain ι = ℕ though, I would like something more general.

[Yury G. Kudryashov]

import topology.metric_space.basic

/-!
-/

open filter set metric
open_locale uniformity filter topological_space

variables {α ι : Type*} [pseudo_metric_space α] {f : ι → α} {a : α}

lemma bounded_range_of_tendsto_cofinite_uniformity
  (hf : tendsto (prod.map f f) (cofinite ×ᶠ cofinite) (𝓤 α)) :
  bounded (range f) :=
begin
  rcases (has_basis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one
    with ⟨s, hsf, hs1⟩,
  rw [← image_univ, ← union_compl_self s, image_union, bounded_union],
  use [(hsf.image f).bounded, 1],
  rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩,
  exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)
end

lemma bounded_range_of_cauchy_map_cofinite (hf : cauchy (map f cofinite)) : bounded (range f) :=
bounded_range_of_tendsto_cofinite_uniformity $ (cauchy_map_iff.1 hf).2

lemma bounded_range_of_tendsto_cofinite (hf : tendsto f cofinite (𝓝 a)) : bounded (range f) :=
bounded_range_of_tendsto_cofinite_uniformity $
  (hf.prod_map hf).mono_right $ nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)

[Yury G. Kudryashov]

It needs

lemma has_basis_cofinite : has_basis cofinite (λ s : set α, s.finite) compl :=
+⟨λ s, ⟨λ h, ⟨sᶜ, h, (compl_compl s).subset⟩, λ ⟨t, htf, hts⟩, htf.subset $ compl_subset_comm.2 hts⟩⟩

[Yury G. Kudryashov]

#10423

[Heather Macbeth]

Very nice! It is interesting to me that this proof for the metric version does not obviously translate to a proof for the order version (fine for me, I only need it for the reals).

[Yury G. Kudryashov]

#10424

[Yury G. Kudryashov]

UPD: we have docs#filter.tendsto.is_bounded_under_le.

[Yury G. Kudryashov]

I'm going to adjust #10424 to this API