Infimum separation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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).
!
theorem
set.einfsep_insert_le
{α : Type u_1}
[has_edist α]
{x : α}
{s : set α} :
(has_insert.insert x s).einfsep ≤ ⨅ (y : α) (H : y ∈ s) (hxy : x ≠ y), has_edist.edist x y
theorem
set.le_einfsep_pair
{α : Type u_1}
[has_edist α]
{x y : α} :
has_edist.edist x y ⊓ has_edist.edist y x ≤ {x, y}.einfsep
theorem
set.einfsep_pair_le_left
{α : Type u_1}
[has_edist α]
{x y : α}
(hxy : x ≠ y) :
{x, y}.einfsep ≤ has_edist.edist x y
theorem
set.einfsep_pair_le_right
{α : Type u_1}
[has_edist α]
{x y : α}
(hxy : x ≠ y) :
{x, y}.einfsep ≤ has_edist.edist y x
theorem
set.einfsep_pair_eq_inf
{α : Type u_1}
[has_edist α]
{x y : α}
(hxy : x ≠ y) :
{x, y}.einfsep = has_edist.edist x y ⊓ has_edist.edist y x
theorem
set.einfsep_eq_infi
{α : Type u_1}
[has_edist α]
{s : set α} :
s.einfsep = ⨅ (d : ↥(s.off_diag)), function.uncurry has_edist.edist ↑d
theorem
set.einfsep_of_fintype
{α : Type u_1}
[has_edist α]
{s : set α}
[decidable_eq α]
[fintype ↥s] :
theorem
set.finite.einfsep_exists_of_nontrivial
{α : Type u_1}
[has_edist α]
{s : set α}
(hsf : s.finite)
(hs : s.nontrivial) :
theorem
set.einfsep_pair
{α : Type u_1}
[pseudo_emetric_space α]
{x y : α}
(hxy : x ≠ y) :
{x, y}.einfsep = has_edist.edist x y
theorem
set.einfsep_insert
{α : Type u_1}
[pseudo_emetric_space α]
{x : α}
{s : set α} :
(has_insert.insert x s).einfsep = (⨅ (y : α) (H : y ∈ s) (hxy : x ≠ y), has_edist.edist x y) ⊓ s.einfsep
theorem
set.einfsep_triple
{α : Type u_1}
[pseudo_emetric_space α]
{x y z : α}
(hxy : x ≠ y)
(hyz : y ≠ z)
(hxz : x ≠ z) :
{x, y, z}.einfsep = has_edist.edist x y ⊓ has_edist.edist x z ⊓ has_edist.edist y z
theorem
set.subsingleton_of_einfsep_eq_top
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
(hs : s.einfsep = ⊤) :
theorem
set.einfsep_eq_top_iff
{α : Type u_1}
[pseudo_metric_space α]
{s : set α} :
s.einfsep = ⊤ ↔ s.subsingleton
theorem
set.nontrivial.einfsep_ne_top
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
(hs : s.nontrivial) :
theorem
set.nontrivial.einfsep_lt_top
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
(hs : s.nontrivial) :
theorem
set.einfsep_lt_top_iff
{α : Type u_1}
[pseudo_metric_space α]
{s : set α} :
s.einfsep < ⊤ ↔ s.nontrivial
theorem
set.einfsep_ne_top_iff
{α : Type u_1}
[pseudo_metric_space α]
{s : set α} :
s.einfsep ≠ ⊤ ↔ s.nontrivial
theorem
set.le_einfsep_of_forall_dist_le
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
{d : ℝ}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ has_dist.dist x y) :
ennreal.of_real d ≤ s.einfsep
theorem
set.subsingleton.infsep_zero
{α : Type u_1}
[has_edist α]
{s : set α}
(hs : s.subsingleton) :
theorem
set.infsep_pair_le_to_real_inf
{α : Type u_1}
[has_edist α]
{x y : α}
(hxy : x ≠ y) :
{x, y}.infsep ≤ (has_edist.edist x y ⊓ has_edist.edist y x).to_real
theorem
set.infsep_pair_eq_to_real
{α : Type u_1}
[pseudo_emetric_space α]
{x y : α} :
{x, y}.infsep = (has_edist.edist x y).to_real
theorem
set.nontrivial.le_infsep_iff
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
{d : ℝ}
(hs : s.nontrivial) :
theorem
set.nontrivial.infsep_lt_iff
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
{d : ℝ}
(hs : s.nontrivial) :
theorem
set.nontrivial.le_infsep
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
{d : ℝ}
(hs : s.nontrivial)
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ has_dist.dist x y) :
theorem
set.le_edist_of_le_infsep
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
{d : ℝ}
{x : α}
(hx : x ∈ s)
{y : α}
(hy : y ∈ s)
(hxy : x ≠ y)
(hd : d ≤ s.infsep) :
d ≤ has_dist.dist x y
theorem
set.infsep_le_dist_of_mem
{α : Type u_1}
[pseudo_metric_space α]
{x y : α}
{s : set α}
(hx : x ∈ s)
(hy : y ∈ s)
(hxy : x ≠ y) :
s.infsep ≤ has_dist.dist x y
theorem
set.infsep_le_of_mem_of_edist_le
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
{d : ℝ}
{x : α}
(hx : x ∈ s)
{y : α}
(hy : y ∈ s)
(hxy : x ≠ y)
(hxy' : has_dist.dist x y ≤ d) :
theorem
set.infsep_pair
{α : Type u_1}
[pseudo_metric_space α]
{x y : α} :
{x, y}.infsep = has_dist.dist x y
theorem
set.infsep_triple
{α : Type u_1}
[pseudo_metric_space α]
{x y z : α}
(hxy : x ≠ y)
(hyz : y ≠ z)
(hxz : x ≠ z) :
{x, y, z}.infsep = has_dist.dist x y ⊓ has_dist.dist x z ⊓ has_dist.dist y z
theorem
set.nontrivial.infsep_anti
{α : Type u_1}
[pseudo_metric_space α]
{s t : set α}
(hs : s.nontrivial)
(hst : s ⊆ t) :
theorem
set.infsep_eq_infi
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
[decidable s.nontrivial] :
s.infsep = ite s.nontrivial (⨅ (d : ↥(s.off_diag)), function.uncurry has_dist.dist ↑d) 0
theorem
set.nontrivial.infsep_eq_infi
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
(hs : s.nontrivial) :
s.infsep = ⨅ (d : ↥(s.off_diag)), function.uncurry has_dist.dist ↑d
theorem
set.infsep_of_fintype
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
[decidable s.nontrivial]
[decidable_eq α]
[fintype ↥s] :
s.infsep = dite s.nontrivial (λ (hs : s.nontrivial), s.off_diag.to_finset.inf' _ (function.uncurry has_dist.dist)) (λ (hs : ¬s.nontrivial), 0)
theorem
set.nontrivial.infsep_of_fintype
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
[decidable_eq α]
[fintype ↥s]
(hs : s.nontrivial) :
theorem
set.finite.infsep
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
[decidable s.nontrivial]
(hsf : s.finite) :
s.infsep = dite s.nontrivial (λ (hs : s.nontrivial), _.to_finset.inf' _ (function.uncurry has_dist.dist)) (λ (hs : ¬s.nontrivial), 0)
theorem
set.finite.infsep_of_nontrivial
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
(hsf : s.finite)
(hs : s.nontrivial) :
s.infsep = _.to_finset.inf' _ (function.uncurry has_dist.dist)
theorem
finset.coe_infsep_of_off_diag_nonempty
{α : Type u_1}
[pseudo_metric_space α]
[decidable_eq α]
{s : finset α}
(hs : s.off_diag.nonempty) :
↑s.infsep = s.off_diag.inf' hs (function.uncurry has_dist.dist)
theorem
finset.coe_infsep_of_off_diag_empty
{α : Type u_1}
[pseudo_metric_space α]
[decidable_eq α]
{s : finset α}
(hs : s.off_diag = ∅) :
theorem
set.nontrivial.infsep_exists_of_finite
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
[finite ↥s]
(hs : s.nontrivial) :
theorem
set.finite.infsep_exists_of_nontrivial
{α : Type u_1}
[pseudo_metric_space α]
{s : set α}
(hsf : s.finite)
(hs : s.nontrivial) :
theorem
set.infsep_zero_iff_subsingleton_of_finite
{α : Type u_1}
[metric_space α]
{s : set α}
[finite ↥s] :
s.infsep = 0 ↔ s.subsingleton
theorem
set.infsep_pos_iff_nontrivial_of_finite
{α : Type u_1}
[metric_space α]
{s : set α}
[finite ↥s] :
0 < s.infsep ↔ s.nontrivial
theorem
set.finite.infsep_zero_iff_subsingleton
{α : Type u_1}
[metric_space α]
{s : set α}
(hs : s.finite) :
s.infsep = 0 ↔ s.subsingleton
theorem
set.finite.infsep_pos_iff_nontrivial
{α : Type u_1}
[metric_space α]
{s : set α}
(hs : s.finite) :
0 < s.infsep ↔ s.nontrivial