Filter.Tendsto.exists_isBounded_image

Stream: Is there code for X?

[Jireh Loreaux]

I can't find this, but perhaps my phrasing is just off. I can't imagine that we really don't have it though. Note: I'm aware of the existence of docs#Filter.Tendsto.isBoundedUnder_le, and while you could use that to get this, it's not really any easier.

import Mathlib.Topology.MetricSpace.Bounded

open Bornology Metric Topology

theorem Filter.Tendsto.exists_isBounded_image {α β : Type*} [PseudoMetricSpace β]
    {l : Filter α} {f : α → β} {x : β} (hf : Tendsto f l (𝓝 x)) :
    ∃ s ∈ l, IsBounded (f '' s)  := by
  refine ⟨_, hf <| nhds_basis_ball.mem_of_mem zero_lt_one, ?_⟩
  apply Metric.isBounded_ball (x := x) (r := 1) |>.subset
  rintro - ⟨y, hy, rfl⟩
  exact hy

[Yury G. Kudryashov]

This should follow from disjoint (nhds _) (cobounded _).

[Yury G. Kudryashov]

And docs#Filter.HasBasis.disjoint_iff_left

[Yury G. Kudryashov]

Something like (l.basis_sets.map _).disjoint_iff_left.1 ((disjoint_nhds_cobounded _).mono_left hf) (not tested)

[Yury G. Kudryashov]

Probably with compl_mem_cobounded

[Yury G. Kudryashov]

The only reason I like this strangely looking proof more than yours is that we may want to add typeclasses for "topology plays nicely with bornology" later if we have some use cases.

[Yury G. Kudryashov]

And if we do this, it may be useful to see which basis properties (like "nhds are bounded") were used in the proof.