Infimum separation

This file defines the extended infimum separation of a set. This is approximately dual to the diameter of a set, but where the extended diameter of a set is the supremum of the extended distance between elements of the set, the extended infimum separation is the infimum of the (extended) distance between distinct elements in the set.

We also define the infimum separation as the cast of the extended infimum separation to the reals. This is the infimum of the distance between distinct elements of the set when in a pseudometric space.

All lemmas and definitions are in the Set namespace to give access to dot notation.

Main definitions

• Set.einfsep: Extended infimum separation of a set.
• Set.infsep: Infimum separation of a set (when in a pseudometric space).

!

noncomputable def Set.einfsep {α : Type u_1} [EDist α] (s : Set α) : ENNReal

The "extended infimum separation" of a set with an edist function.

Equations

• s.einfsep = ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

theorem Set.le_einfsep_iff {α : Type u_1} [EDist α] {s : Set α} {d : ENNReal} : d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y

theorem Set.einfsep_zero {α : Type u_1} [EDist α] {s : Set α} : s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

theorem Set.einfsep_pos {α : Type u_1} [EDist α] {s : Set α} : 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

theorem Set.einfsep_top {α : Type u_1} [EDist α] {s : Set α} : s.einfsep = ⊤ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤

theorem Set.einfsep_lt_top {α : Type u_1} [EDist α] {s : Set α} : s.einfsep < ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ⊤

theorem Set.einfsep_ne_top {α : Type u_1} [EDist α] {s : Set α} : s.einfsep ≠ ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ⊤

theorem Set.einfsep_lt_iff {α : Type u_1} [EDist α] {s : Set α} {d : ENNReal} : s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

theorem Set.nontrivial_of_einfsep_lt_top {α : Type u_1} [EDist α] {s : Set α} (hs : s.einfsep < ⊤) : s.Nontrivial

theorem Set.nontrivial_of_einfsep_ne_top {α : Type u_1} [EDist α] {s : Set α} (hs : s.einfsep ≠ ⊤) : s.Nontrivial

theorem Set.Subsingleton.einfsep {α : Type u_1} [EDist α] {s : Set α} (hs : s.Subsingleton) : s.einfsep = ⊤

theorem Set.le_einfsep_image_iff {α : Type u_1} {β : Type u_2} [EDist α] {d : ENNReal} {f : β → α} {s : Set β} : d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

theorem Set.le_edist_of_le_einfsep {α : Type u_1} [EDist α] {s : Set α} {d : ENNReal} {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) (hxy : x ≠ y) (hd : d ≤ s.einfsep) : d ≤ edist x y

theorem Set.einfsep_le_edist_of_mem {α : Type u_1} [EDist α] {s : Set α} {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) (hxy : x ≠ y) : s.einfsep ≤ edist x y

theorem Set.einfsep_le_of_mem_of_edist_le {α : Type u_1} [EDist α] {s : Set α} {d : ENNReal} {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) (hxy : x ≠ y) (hxy' : edist x y ≤ d) : s.einfsep ≤ d

theorem Set.le_einfsep {α : Type u_1} [EDist α] {s : Set α} {d : ENNReal} (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y) : d ≤ s.einfsep

@[simp]

theorem Set.einfsep_empty {α : Type u_1} [EDist α] : ∅.einfsep = ⊤

@[simp]

theorem Set.einfsep_singleton {α : Type u_1} [EDist α] {x : α} : {x}.einfsep = ⊤

theorem Set.einfsep_iUnion_mem_option {α : Type u_1} [EDist α] {ι : Type u_3} (o : Option ι) (s : ι → Set α) : (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep

theorem Set.einfsep_anti {α : Type u_1} [EDist α] {s : Set α} {t : Set α} (hst : s ⊆ t) : t.einfsep ≤ s.einfsep

theorem Set.einfsep_insert_le {α : Type u_1} [EDist α] {x : α} {s : Set α} : (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

theorem Set.le_einfsep_pair {α : Type u_1} [EDist α] {x : α} {y : α} : edist x y ⊓ edist y x ≤ {x, y}.einfsep

theorem Set.einfsep_pair_le_left {α : Type u_1} [EDist α] {x : α} {y : α} (hxy : x ≠ y) : {x, y}.einfsep ≤ edist x y

theorem Set.einfsep_pair_le_right {α : Type u_1} [EDist α] {x : α} {y : α} (hxy : x ≠ y) : {x, y}.einfsep ≤ edist y x

theorem Set.einfsep_pair_eq_inf {α : Type u_1} [EDist α] {x : α} {y : α} (hxy : x ≠ y) : {x, y}.einfsep = edist x y ⊓ edist y x

theorem Set.einfsep_eq_iInf {α : Type u_1} [EDist α] {s : Set α} : s.einfsep = ⨅ (d : ↑s.offDiag), Function.uncurry edist ↑d

theorem Set.einfsep_of_fintype {α : Type u_1} [EDist α] {s : Set α} [DecidableEq α] [Fintype ↑s] : s.einfsep = s.offDiag.toFinset.inf (Function.uncurry edist)

theorem Set.Finite.einfsep {α : Type u_1} [EDist α] {s : Set α} (hs : s.Finite) : s.einfsep = ⋯.toFinset.inf (Function.uncurry edist)

theorem Set.Finset.coe_einfsep {α : Type u_1} [EDist α] [DecidableEq α] {s : Finset α} : (↑s).einfsep = s.offDiag.inf (Function.uncurry edist)

theorem Set.Nontrivial.einfsep_exists_of_finite {α : Type u_1} [EDist α] {s : Set α} [Finite ↑s] (hs : s.Nontrivial) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

theorem Set.Finite.einfsep_exists_of_nontrivial {α : Type u_1} [EDist α] {s : Set α} (hsf : s.Finite) (hs : s.Nontrivial) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

theorem Set.einfsep_pair {α : Type u_1} [PseudoEMetricSpace α] {x : α} {y : α} (hxy : x ≠ y) : {x, y}.einfsep = edist x y

theorem Set.einfsep_insert {α : Type u_1} [PseudoEMetricSpace α] {x : α} {s : Set α} : (insert x s).einfsep = (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep

theorem Set.einfsep_triple {α : Type u_1} [PseudoEMetricSpace α] {x : α} {y : α} {z : α} (hxy : x ≠ y) (hyz : y ≠ z) (hxz : x ≠ z) : {x, y, z}.einfsep = edist x y ⊓ edist x z ⊓ edist y z

theorem Set.le_einfsep_pi_of_le {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoEMetricSpace (π b)] {s : (b : β) → Set (π b)} {c : ENNReal} (h : ∀ (b : β), c ≤ (s b).einfsep) : c ≤ (Set.univ.pi s).einfsep

theorem Set.subsingleton_of_einfsep_eq_top {α : Type u_1} [PseudoMetricSpace α] {s : Set α} (hs : s.einfsep = ⊤) : s.Subsingleton

theorem Set.einfsep_eq_top_iff {α : Type u_1} [PseudoMetricSpace α] {s : Set α} : s.einfsep = ⊤ ↔ s.Subsingleton

theorem Set.Nontrivial.einfsep_ne_top {α : Type u_1} [PseudoMetricSpace α] {s : Set α} (hs : s.Nontrivial) : s.einfsep ≠ ⊤

theorem Set.Nontrivial.einfsep_lt_top {α : Type u_1} [PseudoMetricSpace α] {s : Set α} (hs : s.Nontrivial) : s.einfsep < ⊤

theorem Set.einfsep_lt_top_iff {α : Type u_1} [PseudoMetricSpace α] {s : Set α} : s.einfsep < ⊤ ↔ s.Nontrivial

theorem Set.einfsep_ne_top_iff {α : Type u_1} [PseudoMetricSpace α] {s : Set α} : s.einfsep ≠ ⊤ ↔ s.Nontrivial

theorem Set.le_einfsep_of_forall_dist_le {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {d : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y) : ENNReal.ofReal d ≤ s.einfsep

theorem Set.einfsep_pos_of_finite {α : Type u_1} [EMetricSpace α] {s : Set α} [Finite ↑s] : 0 < s.einfsep

theorem Set.relatively_discrete_of_finite {α : Type u_1} [EMetricSpace α] {s : Set α} [Finite ↑s] : ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

theorem Set.Finite.einfsep_pos {α : Type u_1} [EMetricSpace α] {s : Set α} (hs : s.Finite) : 0 < s.einfsep

theorem Set.Finite.relatively_discrete {α : Type u_1} [EMetricSpace α] {s : Set α} (hs : s.Finite) : ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

noncomputable def Set.infsep {α : Type u_1} [EDist α] (s : Set α) : ℝ

The "infimum separation" of a set with an edist function.

Equations

• s.infsep = s.einfsep.toReal

theorem Set.infsep_zero {α : Type u_1} [EDist α] {s : Set α} : s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ⊤

theorem Set.infsep_nonneg {α : Type u_1} [EDist α] {s : Set α} : 0 ≤ s.infsep

theorem Set.infsep_pos {α : Type u_1} [EDist α] {s : Set α} : 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ⊤

theorem Set.Subsingleton.infsep_zero {α : Type u_1} [EDist α] {s : Set α} (hs : s.Subsingleton) : s.infsep = 0

theorem Set.nontrivial_of_infsep_pos {α : Type u_1} [EDist α] {s : Set α} (hs : 0 < s.infsep) : s.Nontrivial

theorem Set.infsep_empty {α : Type u_1} [EDist α] : ∅.infsep = 0

theorem Set.infsep_singleton {α : Type u_1} [EDist α] {x : α} : {x}.infsep = 0

theorem Set.infsep_pair_le_toReal_inf {α : Type u_1} [EDist α] {x : α} {y : α} (hxy : x ≠ y) : {x, y}.infsep ≤ (edist x y ⊓ edist y x).toReal

theorem Set.infsep_pair_eq_toReal {α : Type u_1} [PseudoEMetricSpace α] {x : α} {y : α} : {x, y}.infsep = (edist x y).toReal

theorem Set.Nontrivial.le_infsep_iff {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {d : ℝ} (hs : s.Nontrivial) : d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

theorem Set.Nontrivial.infsep_lt_iff {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {d : ℝ} (hs : s.Nontrivial) : s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

theorem Set.Nontrivial.le_infsep {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {d : ℝ} (hs : s.Nontrivial) (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y) : d ≤ s.infsep

theorem Set.le_edist_of_le_infsep {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {d : ℝ} {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) (hxy : x ≠ y) (hd : d ≤ s.infsep) : d ≤ dist x y

theorem Set.infsep_le_dist_of_mem {α : Type u_1} [PseudoMetricSpace α] {x : α} {y : α} {s : Set α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : s.infsep ≤ dist x y

theorem Set.infsep_le_of_mem_of_edist_le {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {d : ℝ} {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) (hxy : x ≠ y) (hxy' : dist x y ≤ d) : s.infsep ≤ d

theorem Set.infsep_pair {α : Type u_1} [PseudoMetricSpace α] {x : α} {y : α} : {x, y}.infsep = dist x y

theorem Set.infsep_triple {α : Type u_1} [PseudoMetricSpace α] {x : α} {y : α} {z : α} (hxy : x ≠ y) (hyz : y ≠ z) (hxz : x ≠ z) : {x, y, z}.infsep = dist x y ⊓ dist x z ⊓ dist y z

theorem Set.Nontrivial.infsep_anti {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {t : Set α} (hs : s.Nontrivial) (hst : s ⊆ t) : t.infsep ≤ s.infsep

theorem Set.infsep_eq_iInf {α : Type u_1} [PseudoMetricSpace α] {s : Set α} [Decidable s.Nontrivial] : s.infsep = if s.Nontrivial then ⨅ (d : ↑s.offDiag), Function.uncurry dist ↑d else 0

theorem Set.Nontrivial.infsep_eq_iInf {α : Type u_1} [PseudoMetricSpace α] {s : Set α} (hs : s.Nontrivial) : s.infsep = ⨅ (d : ↑s.offDiag), Function.uncurry dist ↑d

theorem Set.infsep_of_fintype {α : Type u_1} [PseudoMetricSpace α] {s : Set α} [Decidable s.Nontrivial] [DecidableEq α] [Fintype ↑s] : s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (Function.uncurry dist) else 0

theorem Set.Nontrivial.infsep_of_fintype {α : Type u_1} [PseudoMetricSpace α] {s : Set α} [DecidableEq α] [Fintype ↑s] (hs : s.Nontrivial) : s.infsep = s.offDiag.toFinset.inf' ⋯ (Function.uncurry dist)

theorem Set.Finite.infsep {α : Type u_1} [PseudoMetricSpace α] {s : Set α} [Decidable s.Nontrivial] (hsf : s.Finite) : s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (Function.uncurry dist) else 0

theorem Set.Finite.infsep_of_nontrivial {α : Type u_1} [PseudoMetricSpace α] {s : Set α} (hsf : s.Finite) (hs : s.Nontrivial) : s.infsep = ⋯.toFinset.inf' ⋯ (Function.uncurry dist)

theorem Finset.coe_infsep {α : Type u_1} [PseudoMetricSpace α] [DecidableEq α] (s : Finset α) : (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (Function.uncurry dist) else 0

theorem Finset.coe_infsep_of_offDiag_nonempty {α : Type u_1} [PseudoMetricSpace α] [DecidableEq α] {s : Finset α} (hs : s.offDiag.Nonempty) : (↑s).infsep = s.offDiag.inf' hs (Function.uncurry dist)

theorem Finset.coe_infsep_of_offDiag_empty {α : Type u_1} [PseudoMetricSpace α] [DecidableEq α] {s : Finset α} (hs : s.offDiag = ∅) : (↑s).infsep = 0

theorem Set.Nontrivial.infsep_exists_of_finite {α : Type u_1} [PseudoMetricSpace α] {s : Set α} [Finite ↑s] (hs : s.Nontrivial) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

theorem Set.Finite.infsep_exists_of_nontrivial {α : Type u_1} [PseudoMetricSpace α] {s : Set α} (hsf : s.Finite) (hs : s.Nontrivial) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

theorem Set.infsep_zero_iff_subsingleton_of_finite {α : Type u_1} [MetricSpace α] {s : Set α} [Finite ↑s] : s.infsep = 0 ↔ s.Subsingleton

theorem Set.infsep_pos_iff_nontrivial_of_finite {α : Type u_1} [MetricSpace α] {s : Set α} [Finite ↑s] : 0 < s.infsep ↔ s.Nontrivial

theorem Set.Finite.infsep_zero_iff_subsingleton {α : Type u_1} [MetricSpace α] {s : Set α} (hs : s.Finite) : s.infsep = 0 ↔ s.Subsingleton

theorem Set.Finite.infsep_pos_iff_nontrivial {α : Type u_1} [MetricSpace α] {s : Set α} (hs : s.Finite) : 0 < s.infsep ↔ s.Nontrivial

theorem Finset.infsep_zero_iff_subsingleton {α : Type u_1} [MetricSpace α] (s : Finset α) : (↑s).infsep = 0 ↔ (↑s).Subsingleton

theorem Finset.infsep_pos_iff_nontrivial {α : Type u_1} [MetricSpace α] (s : Finset α) : 0 < (↑s).infsep ↔ (↑s).Nontrivial