Documentation

Mathlib.Topology.MetricSpace.Bounded

Boundedness in (pseudo)-metric spaces #

This file contains one definition, and various results on boundedness in pseudo-metric spaces.

Tags #

metric, pseudo_metric, bounded, diameter, Heine-Borel theorem

Closed balls are bounded

Open balls are bounded

Spheres are bounded

Given a point, a bounded subset is included in some ball around this point

theorem Bornology.IsBounded.subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (c : α) :
∃ (r : ), s Metric.closedBall c r
theorem Bornology.IsBounded.subset_ball_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (a : ) (c : α) :
∃ (r : ), a < r s Metric.ball c r
theorem Bornology.IsBounded.subset_ball {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (c : α) :
∃ (r : ), s Metric.ball c r
theorem Metric.isBounded_iff_subset_ball {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : α) :
theorem Bornology.IsBounded.subset_closedBall_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (a : ) (c : α) :
∃ (r : ), a < r s Metric.closedBall c r
theorem Metric.hasBasis_cobounded_compl_closedBall {α : Type u} [PseudoMetricSpace α] (c : α) :
(Bornology.cobounded α).HasBasis (fun (x : ) => True) fun (r : ) => (Metric.closedBall c r)
theorem Metric.hasBasis_cobounded_compl_ball {α : Type u} [PseudoMetricSpace α] (c : α) :
(Bornology.cobounded α).HasBasis (fun (x : ) => True) fun (r : ) => (Metric.ball c r)
@[simp]
theorem Metric.comap_dist_right_atTop {α : Type u} [PseudoMetricSpace α] (c : α) :
Filter.comap (fun (x : α) => dist x c) Filter.atTop = Bornology.cobounded α
@[simp]
theorem Metric.comap_dist_left_atTop {α : Type u} [PseudoMetricSpace α] (c : α) :
@[simp]
theorem Metric.tendsto_dist_right_atTop_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] (c : α) {f : βα} {l : Filter β} :
Filter.Tendsto (fun (x : β) => dist (f x) c) l Filter.atTop Filter.Tendsto f l (Bornology.cobounded α)
@[simp]
theorem Metric.tendsto_dist_left_atTop_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] (c : α) {f : βα} {l : Filter β} :
Filter.Tendsto (fun (x : β) => dist c (f x)) l Filter.atTop Filter.Tendsto f l (Bornology.cobounded α)
theorem Metric.tendsto_dist_right_cobounded_atTop {α : Type u} [PseudoMetricSpace α] (c : α) :
Filter.Tendsto (fun (x : α) => dist x c) (Bornology.cobounded α) Filter.atTop

A totally bounded set is bounded

A compact set is bounded

theorem Metric.isBounded_range_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} :
Bornology.IsBounded (Set.range f) ∃ (C : ), ∀ (x y : β), dist (f x) (f y) C

Characterization of the boundedness of the range of a function

theorem Metric.isBounded_image_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} {s : Set β} :
Bornology.IsBounded (f '' s) ∃ (C : ), xs, ys, dist (f x) (f y) C
theorem Metric.isBounded_range_of_tendsto_cofinite_uniformity {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} (hf : Filter.Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (uniformity α)) :
theorem Metric.isBounded_range_of_cauchy_map_cofinite {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} (hf : Cauchy (Filter.map f Filter.cofinite)) :
theorem Metric.isBounded_range_of_tendsto_cofinite {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} {a : α} (hf : Filter.Tendsto f Filter.cofinite (nhds a)) :

In a compact space, all sets are bounded

theorem Metric.isBounded_range_of_tendsto {α : Type u} [PseudoMetricSpace α] (u : α) {x : α} (hu : Filter.Tendsto u Filter.atTop (nhds x)) :
theorem Metric.exists_isBounded_image_of_tendsto {α : Type u_3} {β : Type u_4} [PseudoMetricSpace β] {l : Filter α} {f : αβ} {x : β} (hf : Filter.Tendsto f l (nhds x)) :
sl, Bornology.IsBounded (f '' s)
theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : βα} (hk : IsCompact k) (hf : xk, ContinuousWithinAt f s x) :
∃ (t : Set β), k t IsOpen t Bornology.IsBounded (f '' (t s))

If a function is continuous within a set s at every point of a compact set k, then it is bounded on some open neighborhood of k in s.

theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {f : βα} (hk : IsCompact k) (hf : xk, ContinuousAt f x) :
∃ (t : Set β), k t IsOpen t Bornology.IsBounded (f '' t)

If a function is continuous at every point of a compact set k, then it is bounded on some open neighborhood of k.

theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : βα} (hk : IsCompact k) (hks : k s) (hf : ContinuousOn f s) :
∃ (t : Set β), k t IsOpen t Bornology.IsBounded (f '' (t s))

If a function is continuous on a set s containing a compact set k, then it is bounded on some open neighborhood of k in s.

theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : βα} (hk : IsCompact k) (hs : IsOpen s) (hks : k s) (hf : ContinuousOn f s) :
∃ (t : Set β), k t IsOpen t Bornology.IsBounded (f '' t)

If a function is continuous on a neighborhood of a compact set k, then it is bounded on some open neighborhood of k.

The Heine–Borel theorem: In a proper space, a closed bounded set is compact.

The Heine–Borel theorem: In a proper space, the closure of a bounded set is compact.

The Heine–Borel theorem: In a proper Hausdorff space, a set is compact if and only if it is closed and bounded.

theorem totallyBounded_Icc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
theorem totallyBounded_Ico {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
theorem totallyBounded_Ioc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
theorem totallyBounded_Ioo {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :

In a pseudo metric space with a conditionally complete linear order such that the order and the metric structure give the same topology, any order-bounded set is metric-bounded.

noncomputable def Metric.diam {α : Type u} [PseudoMetricSpace α] (s : Set α) :

The diameter of a set in a metric space. To get controllable behavior even when the diameter should be infinite, we express it in terms of the EMetric.diam

Equations
Instances For
    theorem Metric.diam_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} :

    The diameter of a set is always nonnegative

    theorem Metric.diam_subsingleton {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : s.Subsingleton) :
    @[simp]

    The empty set has zero diameter

    @[simp]
    theorem Metric.diam_singleton {α : Type u} [PseudoMetricSpace α] {x : α} :

    A singleton has zero diameter

    @[simp]
    theorem Metric.diam_zero {α : Type u} [PseudoMetricSpace α] [Zero α] :
    @[simp]
    theorem Metric.diam_one {α : Type u} [PseudoMetricSpace α] [One α] :
    theorem Metric.diam_pair {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
    Metric.diam {x, y} = dist x y
    theorem Metric.diam_triple {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {z : α} :
    Metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
    theorem Metric.ediam_le_of_forall_dist_le {α : Type u} [PseudoMetricSpace α] {s : Set α} {C : } (h : xs, ys, dist x y C) :

    If the distance between any two points in a set is bounded by some constant C, then ENNReal.ofReal C bounds the emetric diameter of this set.

    theorem Metric.diam_le_of_forall_dist_le {α : Type u} [PseudoMetricSpace α] {s : Set α} {C : } (h₀ : 0 C) (h : xs, ys, dist x y C) :

    If the distance between any two points in a set is bounded by some non-negative constant, this constant bounds the diameter.

    theorem Metric.diam_le_of_forall_dist_le_of_nonempty {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : s.Nonempty) {C : } (h : xs, ys, dist x y C) :

    If the distance between any two points in a nonempty set is bounded by some constant, this constant bounds the diameter.

    theorem Metric.dist_le_diam_of_mem' {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : EMetric.diam s ) (hx : x s) (hy : y s) :

    The distance between two points in a set is controlled by the diameter of the set.

    Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

    Alias of the forward direction of Metric.isBounded_iff_ediam_ne_top.


    Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

    theorem Metric.dist_le_diam_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : Bornology.IsBounded s) (hx : x s) (hy : y s) :

    The distance between two points in a set is controlled by the diameter of the set.

    An unbounded set has zero diameter. If you would prefer to get the value ∞, use EMetric.diam. This lemma makes it possible to avoid side conditions in some situations

    theorem Metric.diam_mono {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (h : s t) (ht : Bornology.IsBounded t) :

    If s ⊆ t, then the diameter of s is bounded by that of t, provided t is bounded.

    theorem Metric.diam_union {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} {t : Set α} (xs : x s) (yt : y t) :

    The diameter of a union is controlled by the sum of the diameters, and the distance between any two points in each of the sets. This lemma is true without any side condition, since it is obviously true if s ∪ t is unbounded.

    theorem Metric.diam_union' {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (h : (s t).Nonempty) :

    If two sets intersect, the diameter of the union is bounded by the sum of the diameters.

    theorem Metric.diam_le_of_subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : } (hr : 0 r) (h : s Metric.closedBall x r) :
    theorem Metric.diam_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {r : } (h : 0 r) :

    The diameter of a closed ball of radius r is at most 2 r.

    theorem Metric.diam_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r : } (h : 0 r) :

    The diameter of a ball of radius r is at most 2 r.

    theorem IsComplete.nonempty_iInter_of_nonempty_biInter {α : Type u} [PseudoMetricSpace α] {s : Set α} (h0 : IsComplete (s 0)) (hs : ∀ (n : ), IsClosed (s n)) (h's : ∀ (n : ), Bornology.IsBounded (s n)) (h : ∀ (N : ), (⋂ (n : ), ⋂ (_ : n N), s n).Nonempty) (h' : Filter.Tendsto (fun (n : ) => Metric.diam (s n)) Filter.atTop (nhds 0)) :
    (⋂ (n : ), s n).Nonempty

    If a family of complete sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

    theorem Metric.nonempty_iInter_of_nonempty_biInter {α : Type u} [PseudoMetricSpace α] [CompleteSpace α] {s : Set α} (hs : ∀ (n : ), IsClosed (s n)) (h's : ∀ (n : ), Bornology.IsBounded (s n)) (h : ∀ (N : ), (⋂ (n : ), ⋂ (_ : n N), s n).Nonempty) (h' : Filter.Tendsto (fun (n : ) => Metric.diam (s n)) Filter.atTop (nhds 0)) :
    (⋂ (n : ), s n).Nonempty

    In a complete space, if a family of closed sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

    Extension for the positivity tactic: the diameter of a set is always nonnegative.

    Instances For
      theorem tendsto_dist_right_cocompact_atTop {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) :
      Filter.Tendsto (fun (x_1 : α) => dist x_1 x) (Filter.cocompact α) Filter.atTop
      theorem tendsto_cocompact_of_tendsto_dist_comp_atTop {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} {l : Filter β} (x : α) (h : Filter.Tendsto (fun (y : β) => dist (f y) x) l Filter.atTop) :
      theorem Metric.finite_isBounded_inter_isClosed {α : Type u} [PseudoMetricSpace α] [ProperSpace α] {K : Set α} {s : Set α} [DiscreteTopology s] (hK : Bornology.IsBounded K) (hs : IsClosed s) :
      (K s).Finite