doc-next-gen

Mathlib.Topology.EMetricSpace.Diam

Module docstring

{"# Diameters of sets in extended metric spaces

"}

EMetric.diam definition
(s : Set α)
Full source 
/-- The diameter of a set in a pseudoemetric space, named `EMetric.diam` -/
noncomputable def diam (s : Set α) :=
  ⨆ (x ∈ s) (y ∈ s), edist x y
Diameter of a set in an extended metric space
Informal description
The diameter of a set $s$ in an extended metric space is the supremum of the extended distances between all pairs of points in $s$, defined as $\mathrm{diam}(s) = \bigsqcup_{x \in s} \bigsqcup_{y \in s} \mathrm{edist}(x, y)$.
EMetric.diam_eq_sSup theorem
(s : Set α) : diam s = sSup (image2 edist s s)
Full source 
theorem diam_eq_sSup (s : Set α) : diam s = sSup (image2 edist s s) := sSup_image2.symm
Diameter as Supremum of Pairwise Distances in Extended Metric Space
Informal description
For any set $s$ in an extended metric space, the diameter of $s$ is equal to the supremum of the extended distances between all pairs of points in $s$, i.e., \[ \mathrm{diam}(s) = \sup \{ \mathrm{edist}(x, y) \mid x \in s, y \in s \}. \]
EMetric.diam_le_iff theorem
{d : ℝ≥0∞} : diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
Full source 
theorem diam_le_iff {d : ℝ≥0∞} : diamdiam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d := by
  simp only [diam, iSup_le_iff]
Characterization of Diameter Bound in Extended Metric Spaces
Informal description
For any extended nonnegative real number $d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the diameter of a set $s$ in an extended metric space is less than or equal to $d$ if and only if for all pairs of points $x, y \in s$, the extended distance between $x$ and $y$ is less than or equal to $d$. In symbols: \[ \mathrm{diam}(s) \leq d \leftrightarrow \forall x \in s, \forall y \in s, \mathrm{edist}(x, y) \leq d. \]
EMetric.diam_image_le_iff theorem
{d : ℝ≥0∞} {f : β → α} {s : Set β} : diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
Full source 
theorem diam_image_le_iff {d : ℝ≥0∞} {f : β → α} {s : Set β} :
    diamdiam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d := by
  simp only [diam_le_iff, forall_mem_image]
Diameter of Image Set Bounded by Extended Distance Condition
Informal description
For an extended nonnegative real number $d$, a function $f : \beta \to \alpha$, and a set $s \subseteq \beta$, the diameter of the image $f(s)$ in the extended metric space is bounded by $d$ if and only if for all $x, y \in s$, the extended distance between $f(x)$ and $f(y)$ is at most $d$. That is, \[ \mathrm{diam}(f(s)) \leq d \leftrightarrow \forall x \in s, \forall y \in s, \mathrm{edist}(f(x), f(y)) \leq d. \]
EMetric.edist_le_of_diam_le theorem
{d} (hx : x ∈ s) (hy : y ∈ s) (hd : diam s ≤ d) : edist x y ≤ d
Full source 
theorem edist_le_of_diam_le {d} (hx : x ∈ s) (hy : y ∈ s) (hd : diam s ≤ d) : edist x y ≤ d :=
  diam_le_iff.1 hd x hx y hy
Extended Distance Bound from Diameter Constraint
Informal description
For any points $x$ and $y$ in a set $s$ in an extended metric space, if the diameter of $s$ is bounded above by an extended nonnegative real number $d$, then the extended distance between $x$ and $y$ is at most $d$. In symbols: \[ x \in s \land y \in s \land \mathrm{diam}(s) \leq d \implies \mathrm{edist}(x, y) \leq d. \]
EMetric.edist_le_diam_of_mem theorem
(hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s
Full source 
/-- If two points belong to some set, their edistance is bounded by the diameter of the set -/
theorem edist_le_diam_of_mem (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s :=
  edist_le_of_diam_le hx hy le_rfl
Extended Distance Bound by Diameter for Points in a Set
Informal description
For any two points $x$ and $y$ in a set $s$ in an extended metric space, the extended distance between $x$ and $y$ is bounded by the diameter of $s$, i.e., \[ x \in s \land y \in s \implies \mathrm{edist}(x, y) \leq \mathrm{diam}(s). \]
EMetric.diam_le theorem
{d : ℝ≥0∞} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : diam s ≤ d
Full source 
/-- If the distance between any two points in a set is bounded by some constant, this constant
bounds the diameter. -/
theorem diam_le {d : ℝ≥0∞} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : diam s ≤ d :=
  diam_le_iff.2 h
Diameter Bound via Pairwise Distance Bound in Extended Metric Spaces
Informal description
For any extended nonnegative real number $d \in [0, \infty]$, if the extended distance between any two points $x, y$ in a set $s$ is bounded by $d$, then the diameter of $s$ is also bounded by $d$. In symbols: \[ (\forall x \in s, \forall y \in s, \mathrm{edist}(x, y) \leq d) \implies \mathrm{diam}(s) \leq d. \]
EMetric.diam_subsingleton theorem
(hs : s.Subsingleton) : diam s = 0
Full source 
/-- The diameter of a subsingleton vanishes. -/
theorem diam_subsingleton (hs : s.Subsingleton) : diam s = 0 :=
  nonpos_iff_eq_zero.1 <| diam_le fun _x hx y hy => (hs hx hy).symm ▸ edist_self y ▸ le_rfl
Vanishing Diameter of Subsingleton Sets in Extended Metric Spaces
Informal description
For any subsingleton set $s$ in an extended metric space, the diameter of $s$ is zero, i.e., $\mathrm{diam}(s) = 0$.
EMetric.diam_empty theorem
: diam (∅ : Set α) = 0
Full source 
/-- The diameter of the empty set vanishes -/
@[simp]
theorem diam_empty : diam (∅ : Set α) = 0 :=
  diam_subsingleton subsingleton_empty
Vanishing Diameter of the Empty Set in Extended Metric Spaces
Informal description
The diameter of the empty set in an extended metric space is zero, i.e., $\mathrm{diam}(\emptyset) = 0$.
EMetric.diam_singleton theorem
: diam ({ x } : Set α) = 0
Full source 
/-- The diameter of a singleton vanishes -/
@[simp]
theorem diam_singleton : diam ({x} : Set α) = 0 :=
  diam_subsingleton subsingleton_singleton
Vanishing Diameter of Singleton Sets in Extended Metric Spaces
Informal description
For any element $x$ in an extended metric space, the diameter of the singleton set $\{x\}$ is zero, i.e., $\mathrm{diam}(\{x\}) = 0$.
EMetric.diam_one theorem
[One α] : diam (1 : Set α) = 0
Full source 
@[to_additive (attr := simp)]
theorem diam_one [One α] : diam (1 : Set α) = 0 :=
  diam_singleton
Vanishing Diameter of the Multiplicative Identity Set in Extended Metric Spaces
Informal description
For any type $\alpha$ with a multiplicative identity element $1$, the diameter of the singleton set $\{1\}$ in an extended metric space is zero, i.e., $\mathrm{diam}(\{1\}) = 0$.
EMetric.diam_iUnion_mem_option theorem
{ι : Type*} (o : Option ι) (s : ι → Set α) : diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i)
Full source 
theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) :
    diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) := by cases o <;> simp
Diameter of Union over Option Indexed Family: $\mathrm{diam}(\bigcup_{i \in o} s_i) = \bigsqcup_{i \in o} \mathrm{diam}(s_i)$
Informal description
For any type $\iota$ and an option $o$ of $\iota$ (i.e., $o$ is either $\text{none}$ or $\text{some } i$ for some $i \in \iota$), and for any family of sets $s : \iota \to \text{Set } \alpha$ in an extended metric space, the diameter of the union $\bigcup_{i \in o} s_i$ is equal to the supremum of the diameters of the sets $s_i$ for $i \in o$. That is, \[ \mathrm{diam}\left(\bigcup_{i \in o} s_i\right) = \bigsqcup_{i \in o} \mathrm{diam}(s_i). \]
EMetric.diam_insert theorem
: diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s)
Full source 
theorem diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) :=
  eq_of_forall_ge_iff fun d => by
    simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff,
      zero_le, true_and, forall_and, and_self_iff, ← and_assoc]
Diameter of Inserted Point Set in Extended Metric Space: $\mathrm{diam}(\{x\} \cup s) = \max(\sup_{y \in s} \mathrm{edist}(x, y), \mathrm{diam}(s))$
Informal description
For any extended metric space and any set $s$ in this space, the diameter of the set obtained by inserting a point $x$ into $s$ is equal to the maximum of the supremum of the extended distances from $x$ to all points in $s$ and the diameter of $s$ itself. That is, \[ \mathrm{diam}(\{x\} \cup s) = \max\left(\sup_{y \in s} \mathrm{edist}(x, y), \mathrm{diam}(s)\right). \]
EMetric.diam_pair theorem
: diam ({ x, y } : Set α) = edist x y
Full source 
theorem diam_pair : diam ({x, y} : Set α) = edist x y := by
  simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right]
Diameter of Two-Point Set in Extended Metric Space: $\mathrm{diam}(\{x, y\}) = \mathrm{edist}(x, y)$
Informal description
For any two points $x$ and $y$ in an extended metric space, the diameter of the set $\{x, y\}$ is equal to the extended distance between $x$ and $y$, i.e., \[ \mathrm{diam}(\{x, y\}) = \mathrm{edist}(x, y). \]
EMetric.diam_triple theorem
: diam ({ x, y, z } : Set α) = max (max (edist x y) (edist x z)) (edist y z)
Full source 
theorem diam_triple : diam ({x, y, z} : Set α) = max (max (edist x y) (edist x z)) (edist y z) := by
  simp only [diam_insert, iSup_insert, iSup_singleton, diam_singleton, ENNReal.max_zero_right]
Diameter of Triple Point Set in Extended Metric Spaces: $\mathrm{diam}(\{x, y, z\}) = \max(\max(\mathrm{edist}(x, y), \mathrm{edist}(x, z)), \mathrm{edist}(y, z))$
Informal description
For any three points $x, y, z$ in an extended metric space, the diameter of the set $\{x, y, z\}$ is equal to the maximum of the extended distances between any two of the points, i.e., \[ \mathrm{diam}(\{x, y, z\}) = \max(\max(\mathrm{edist}(x, y), \mathrm{edist}(x, z)), \mathrm{edist}(y, z)). \]
EMetric.diam_mono theorem
{s t : Set α} (h : s ⊆ t) : diam s ≤ diam t
Full source 
/-- The diameter is monotonous with respect to inclusion -/
@[gcongr]
theorem diam_mono {s t : Set α} (h : s ⊆ t) : diam s ≤ diam t :=
  diam_le fun _x hx _y hy => edist_le_diam_of_mem (h hx) (h hy)
Monotonicity of Diameter with Respect to Inclusion in Extended Metric Spaces
Informal description
For any two sets $s$ and $t$ in an extended metric space, if $s$ is a subset of $t$, then the diameter of $s$ is less than or equal to the diameter of $t$, i.e., \[ s \subseteq t \implies \mathrm{diam}(s) \leq \mathrm{diam}(t). \]
EMetric.diam_union theorem
{t : Set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + edist x y + diam t
Full source 
/-- The diameter of a union is controlled by the diameter of the sets, and the edistance
between two points in the sets. -/
theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
    diam (s ∪ t) ≤ diam s + edist x y + diam t := by
  have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t := fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
      _ ≤ diam s + edist x y + diam t :=
        add_le_add (add_le_add (edist_le_diam_of_mem ha xs) le_rfl) (edist_le_diam_of_mem yt hb)
  refine diam_le fun a ha b hb => ?_
  rcases (mem_union _ _ _).1 ha with h'a | h'a <;> rcases (mem_union _ _ _).1 hb with h'b | h'b
  · calc
      edist a b ≤ diam s := edist_le_diam_of_mem h'a h'b
      _ ≤ diam s + (edist x y + diam t) := le_self_add
      _ = diam s + edist x y + diam t := (add_assoc _ _ _).symm
  · exact A a h'a b h'b
  · have Z := A b h'b a h'a
    rwa [edist_comm] at Z
  · calc
      edist a b ≤ diam t := edist_le_diam_of_mem h'a h'b
      _ ≤ diam s + edist x y + diam t := le_add_self
Diameter Bound for Union of Sets in Extended Metric Spaces: $\mathrm{diam}(s \cup t) \leq \mathrm{diam}(s) + \mathrm{edist}(x, y) + \mathrm{diam}(t)$
Informal description
For any two sets $s$ and $t$ in an extended metric space, and any points $x \in s$ and $y \in t$, the diameter of the union $s \cup t$ is bounded by the sum of the diameters of $s$ and $t$ plus the extended distance between $x$ and $y$, i.e., \[ \mathrm{diam}(s \cup t) \leq \mathrm{diam}(s) + \mathrm{edist}(x, y) + \mathrm{diam}(t). \]
EMetric.diam_union' theorem
{t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t
Full source 
theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t := by
  let ⟨x, ⟨xs, xt⟩⟩ := h
  simpa using diam_union xs xt
Diameter Bound for Union of Overlapping Sets in Extended Metric Spaces: $\mathrm{diam}(s \cup t) \leq \mathrm{diam}(s) + \mathrm{diam}(t)$
Informal description
For any two sets $s$ and $t$ in an extended metric space, if their intersection $s \cap t$ is nonempty, then the diameter of their union satisfies $\mathrm{diam}(s \cup t) \leq \mathrm{diam}(s) + \mathrm{diam}(t)$.
EMetric.diam_closedBall theorem
{r : ℝ≥0∞} : diam (closedBall x r) ≤ 2 * r
Full source 
theorem diam_closedBall {r : ℝ≥0∞} : diam (closedBall x r) ≤ 2 * r :=
  diam_le fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist b x := edist_triangle_right _ _ _
      _ ≤ r + r := add_le_add ha hb
      _ = 2 * r := (two_mul r).symm
Diameter Bound for Closed Balls in Extended Metric Spaces: $\mathrm{diam}(\overline{B}(x, r)) \leq 2r$
Informal description
For any extended nonnegative real number $r \in [0, \infty]$, the diameter of the closed ball centered at $x$ with radius $r$ in an extended metric space is bounded by $2r$, i.e., \[ \mathrm{diam}(\overline{B}(x, r)) \leq 2r. \]
EMetric.diam_ball theorem
{r : ℝ≥0∞} : diam (ball x r) ≤ 2 * r
Full source 
theorem diam_ball {r : ℝ≥0∞} : diam (ball x r) ≤ 2 * r :=
  le_trans (diam_mono ball_subset_closedBall) diam_closedBall
Diameter Bound for Open Balls in Extended Metric Spaces: $\mathrm{diam}(B(x, r)) \leq 2r$
Informal description
For any extended nonnegative real number $r \in [0, \infty]$, the diameter of the open ball centered at $x$ with radius $r$ in an extended metric space is bounded by $2r$, i.e., \[ \mathrm{diam}(B(x, r)) \leq 2r. \]
EMetric.diam_pi_le_of_le theorem
{π : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (π b)] {s : ∀ b : β, Set (π b)} {c : ℝ≥0∞} (h : ∀ b, diam (s b) ≤ c) : diam (Set.pi univ s) ≤ c
Full source 
theorem diam_pi_le_of_le {π : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (π b)]
    {s : ∀ b : β, Set (π b)} {c : ℝ≥0∞} (h : ∀ b, diam (s b) ≤ c) : diam (Set.pi univ s) ≤ c := by
  refine diam_le fun x hx y hy => edist_pi_le_iff.mpr ?_
  rw [mem_univ_pi] at hx hy
  exact fun b => diam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)
Diameter Bound for Product Sets in Extended Metric Spaces
Informal description
Let $\beta$ be a finite type, and for each $b \in \beta$, let $\pi_b$ be a pseudo-extended metric space. Given a family of sets $s_b \subseteq \pi_b$ for each $b \in \beta$ and an extended nonnegative real number $c \in [0, \infty]$, if the diameter of each $s_b$ is bounded by $c$, then the diameter of the product set $\prod_{b \in \beta} s_b$ is also bounded by $c$. In symbols: \[ (\forall b \in \beta, \mathrm{diam}(s_b) \leq c) \implies \mathrm{diam}\left(\prod_{b \in \beta} s_b\right) \leq c. \]
EMetric.diam_eq_zero_iff theorem
: diam s = 0 ↔ s.Subsingleton
Full source 
theorem diam_eq_zero_iff : diamdiam s = 0 ↔ s.Subsingleton :=
  ⟨fun h _x hx _y hy => edist_le_zero.1 <| h ▸ edist_le_diam_of_mem hx hy, diam_subsingleton⟩
Zero Diameter Characterization for Subsingleton Sets in Extended Metric Spaces
Informal description
For any set $s$ in an extended metric space, the diameter of $s$ is zero if and only if $s$ is a subsingleton (i.e., contains at most one point). In other words: \[ \mathrm{diam}(s) = 0 \leftrightarrow \forall x, y \in s, x = y. \]
EMetric.diam_pos_iff theorem
: 0 < diam s ↔ s.Nontrivial
Full source 
theorem diam_pos_iff : 0 < diam s ↔ s.Nontrivial := by
  simp only [pos_iff_ne_zero, Ne, diam_eq_zero_iff, Set.not_subsingleton_iff]
Positive Diameter Characterization for Nontrivial Sets in Extended Metric Spaces
Informal description
For any set $s$ in an extended metric space, the diameter of $s$ is positive if and only if $s$ is nontrivial (i.e., there exist two distinct points in $s$). In other words, $0 < \mathrm{diam}(s) \leftrightarrow \exists x, y \in s, x \neq y$.
EMetric.diam_pos_iff' theorem
: 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Full source 
theorem diam_pos_iff' : 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y := by
  simp only [diam_pos_iff, Set.Nontrivial, exists_prop]
Positive Diameter Criterion for Nontrivial Sets in Extended Metric Spaces
Informal description
For any set $s$ in an extended metric space, the diameter of $s$ is strictly positive if and only if there exist two distinct points $x$ and $y$ in $s$, i.e., $0 < \mathrm{diam}(s) \leftrightarrow \exists x \in s, \exists y \in s, x \neq y$.