Thickenings in pseudo-metric spaces

Main definitions

• Metric.thickening δ s, the open thickening by radius δ of a set s in a pseudo emetric space.
• Metric.cthickening δ s, the closed thickening by radius δ of a set s in a pseudo emetric space.

Main results

• Disjoint.exists_thickenings: two disjoint sets admit disjoint thickenings

• Disjoint.exists_cthickenings: two disjoint sets admit disjoint closed thickenings

• IsCompact.exists_cthickening_subset_open: if s is compact, t is open and s ⊆ t, some cthickening of s is contained in t.

• Metric.hasBasis_nhdsSet_cthickening: the cthickenings of a compact set K form a basis of the neighbourhoods of K

• Metric.closure_eq_iInter_cthickening': the closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero. The same holds for open thickenings.

• IsCompact.cthickening_eq_biUnion_closedBall: if s is compact, cthickening δ s is the union of closedBalls of radius δ around x : E.

def Metric.thickening {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : Set α

The (open) δ-thickening Metric.thickening δ E of a subset E in a pseudo emetric space consists of those points that are at distance less than δ from some point of E.

Equations

• Eq (Metric.thickening δ E) (setOf fun (x : α) => LT.lt (EMetric.infEdist x E) (ENNReal.ofReal δ))

theorem Metric.mem_thickening_iff_infEdist_lt {α : Type u} [PseudoEMetricSpace α] {δ : Real} {s : Set α} {x : α} : Iff (Membership.mem (thickening δ s) x) (LT.lt (EMetric.infEdist x s) (ENNReal.ofReal δ))

theorem Metric.eventually_not_mem_thickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : Not (Membership.mem (closure E) x)) : Filter.Eventually (fun (δ : Real) => Not (Membership.mem (thickening δ E) x)) (nhds 0)

An exterior point of a subset E (i.e., a point outside the closure of E) is not in the (open) δ-thickening of E for small enough positive δ.

theorem Metric.thickening_eq_preimage_infEdist {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : Eq (thickening δ E) (Set.preimage (fun (x : α) => EMetric.infEdist x E) (Set.Iio (ENNReal.ofReal δ)))

The (open) thickening equals the preimage of an open interval under EMetric.infEdist.

theorem Metric.isOpen_thickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} {E : Set α} : IsOpen (thickening δ E)

The (open) thickening is an open set.

theorem Metric.thickening_empty {α : Type u} [PseudoEMetricSpace α] (δ : Real) : Eq (thickening δ EmptyCollection.emptyCollection) EmptyCollection.emptyCollection

The (open) thickening of the empty set is empty.

theorem Metric.thickening_of_nonpos {α : Type u} [PseudoEMetricSpace α] {δ : Real} (hδ : LE.le δ 0) (s : Set α) : Eq (thickening δ s) EmptyCollection.emptyCollection

theorem Metric.thickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ δ₂ : Real} (hle : LE.le δ₁ δ₂) (E : Set α) : HasSubset.Subset (thickening δ₁ E) (thickening δ₂ E)

The (open) thickening Metric.thickening δ E of a fixed subset E is an increasing function of the thickening radius δ.

theorem Metric.thickening_subset_of_subset {α : Type u} [PseudoEMetricSpace α] (δ : Real) {E₁ E₂ : Set α} (h : HasSubset.Subset E₁ E₂) : HasSubset.Subset (thickening δ E₁) (thickening δ E₂)

The (open) thickening Metric.thickening δ E with a fixed thickening radius δ is an increasing function of the subset E.

theorem Metric.mem_thickening_iff_exists_edist_lt {α : Type u} [PseudoEMetricSpace α] {δ : Real} (E : Set α) (x : α) : Iff (Membership.mem (thickening δ E) x) (Exists fun (z : α) => And (Membership.mem E z) (LT.lt (EDist.edist x z) (ENNReal.ofReal δ)))

theorem Metric.frontier_thickening_subset {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : Real} : HasSubset.Subset (frontier (thickening δ E)) (setOf fun (x : α) => Eq (EMetric.infEdist x E) (ENNReal.ofReal δ))

The frontier of the (open) thickening of a set is contained in an EMetric.infEdist level set.

theorem Metric.frontier_thickening_disjoint {α : Type u} [PseudoEMetricSpace α] (A : Set α) : Pairwise (Function.onFun Disjoint fun (r : Real) => frontier (thickening r A))

theorem Metric.subset_compl_thickening_compl_thickening_self {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : HasSubset.Subset E (HasCompl.compl (thickening δ (HasCompl.compl (thickening δ E))))

Any set is contained in the complement of the δ-thickening of the complement of its δ-thickening.

theorem Metric.thickening_compl_thickening_self_subset_compl {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : HasSubset.Subset (thickening δ (HasCompl.compl (thickening δ E))) (HasCompl.compl E)

The δ-thickening of the complement of the δ-thickening of a set is contained in the complement of the set.

theorem Metric.mem_thickening_iff_infDist_lt {δ : Real} {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} (h : E.Nonempty) : Iff (Membership.mem (thickening δ E) x) (LT.lt (infDist x E) δ)

theorem Metric.mem_thickening_iff {δ : Real} {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} : Iff (Membership.mem (thickening δ E) x) (Exists fun (z : X) => And (Membership.mem E z) (LT.lt (Dist.dist x z) δ))

A point in a metric space belongs to the (open) δ-thickening of a subset E if and only if it is at distance less than δ from some point of E.

theorem Metric.thickening_singleton {X : Type u} [PseudoMetricSpace X] (δ : Real) (x : X) : Eq (thickening δ (Singleton.singleton x)) (ball x δ)

theorem Metric.ball_subset_thickening {X : Type u} [PseudoMetricSpace X] {x : X} {E : Set X} (hx : Membership.mem E x) (δ : Real) : HasSubset.Subset (ball x δ) (thickening δ E)

theorem Metric.thickening_eq_biUnion_ball {X : Type u} [PseudoMetricSpace X] {δ : Real} {E : Set X} : Eq (thickening δ E) (Set.iUnion fun (x : X) => Set.iUnion fun (h : Membership.mem E x) => ball x δ)

The (open) δ-thickening Metric.thickening δ E of a subset E in a metric space equals the union of balls of radius δ centered at points of E.

theorem Bornology.IsBounded.thickening {X : Type u} [PseudoMetricSpace X] {δ : Real} {E : Set X} (h : IsBounded E) : IsBounded (Metric.thickening δ E)

def Metric.cthickening {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : Set α

The closed δ-thickening Metric.cthickening δ E of a subset E in a pseudo emetric space consists of those points that are at infimum distance at most δ from E.

Equations

• Eq (Metric.cthickening δ E) (setOf fun (x : α) => LE.le (EMetric.infEdist x E) (ENNReal.ofReal δ))

theorem Metric.mem_cthickening_iff {α : Type u} [PseudoEMetricSpace α] {δ : Real} {s : Set α} {x : α} : Iff (Membership.mem (cthickening δ s) x) (LE.le (EMetric.infEdist x s) (ENNReal.ofReal δ))

theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : Not (Membership.mem (closure E) x)) : Filter.Eventually (fun (δ : Real) => Not (Membership.mem (cthickening δ E) x)) (nhds 0)

An exterior point of a subset E (i.e., a point outside the closure of E) is not in the closed δ-thickening of E for small enough positive δ.

theorem Metric.mem_cthickening_of_edist_le {α : Type u} [PseudoEMetricSpace α] (x y : α) (δ : Real) (E : Set α) (h : Membership.mem E y) (h' : LE.le (EDist.edist x y) (ENNReal.ofReal δ)) : Membership.mem (cthickening δ E) x

theorem Metric.mem_cthickening_of_dist_le {α : Type u_2} [PseudoMetricSpace α] (x y : α) (δ : Real) (E : Set α) (h : Membership.mem E y) (h' : LE.le (Dist.dist x y) δ) : Membership.mem (cthickening δ E) x

theorem Metric.cthickening_eq_preimage_infEdist {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : Eq (cthickening δ E) (Set.preimage (fun (x : α) => EMetric.infEdist x E) (Set.Iic (ENNReal.ofReal δ)))

theorem Metric.isClosed_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} {E : Set α} : IsClosed (cthickening δ E)

The closed thickening is a closed set.

theorem Metric.cthickening_empty {α : Type u} [PseudoEMetricSpace α] (δ : Real) : Eq (cthickening δ EmptyCollection.emptyCollection) EmptyCollection.emptyCollection

The closed thickening of the empty set is empty.

theorem Metric.cthickening_of_nonpos {α : Type u} [PseudoEMetricSpace α] {δ : Real} (hδ : LE.le δ 0) (E : Set α) : Eq (cthickening δ E) (closure E)

theorem Metric.cthickening_zero {α : Type u} [PseudoEMetricSpace α] (E : Set α) : Eq (cthickening 0 E) (closure E)

The closed thickening with radius zero is the closure of the set.

theorem Metric.cthickening_max_zero {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : Eq (cthickening (Max.max 0 δ) E) (cthickening δ E)

theorem Metric.cthickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ δ₂ : Real} (hle : LE.le δ₁ δ₂) (E : Set α) : HasSubset.Subset (cthickening δ₁ E) (cthickening δ₂ E)

The closed thickening Metric.cthickening δ E of a fixed subset E is an increasing function of the thickening radius δ.

theorem Metric.cthickening_singleton {α : Type u_2} [PseudoMetricSpace α] (x : α) {δ : Real} (hδ : LE.le 0 δ) : Eq (cthickening δ (Singleton.singleton x)) (closedBall x δ)

theorem Metric.closedBall_subset_cthickening_singleton {α : Type u_2} [PseudoMetricSpace α] (x : α) (δ : Real) : HasSubset.Subset (closedBall x δ) (cthickening δ (Singleton.singleton x))

theorem Metric.cthickening_subset_of_subset {α : Type u} [PseudoEMetricSpace α] (δ : Real) {E₁ E₂ : Set α} (h : HasSubset.Subset E₁ E₂) : HasSubset.Subset (cthickening δ E₁) (cthickening δ E₂)

The closed thickening Metric.cthickening δ E with a fixed thickening radius δ is an increasing function of the subset E.

theorem Metric.cthickening_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ₁ : NNReal} {δ₂ : Real} (hlt : LT.lt δ₁.toReal δ₂) (E : Set α) : HasSubset.Subset (cthickening δ₁.toReal E) (thickening δ₂ E)

theorem Metric.cthickening_subset_thickening' {α : Type u} [PseudoEMetricSpace α] {δ₁ δ₂ : Real} (δ₂_pos : LT.lt 0 δ₂) (hlt : LT.lt δ₁ δ₂) (E : Set α) : HasSubset.Subset (cthickening δ₁ E) (thickening δ₂ E)

The closed thickening Metric.cthickening δ₁ E is contained in the open thickening Metric.thickening δ₂ E if the radius of the latter is positive and larger.

theorem Metric.thickening_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : HasSubset.Subset (thickening δ E) (cthickening δ E)

The open thickening Metric.thickening δ E is contained in the closed thickening Metric.cthickening δ E with the same radius.

theorem Metric.thickening_subset_cthickening_of_le {α : Type u} [PseudoEMetricSpace α] {δ₁ δ₂ : Real} (hle : LE.le δ₁ δ₂) (E : Set α) : HasSubset.Subset (thickening δ₁ E) (cthickening δ₂ E)

theorem Bornology.IsBounded.cthickening {α : Type u_2} [PseudoMetricSpace α] {δ : Real} {E : Set α} (h : IsBounded E) : IsBounded (Metric.cthickening δ E)

theorem IsCompact.cthickening {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {s : Set α} (hs : IsCompact s) {r : Real} : IsCompact (Metric.cthickening r s)

theorem Metric.thickening_subset_interior_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : HasSubset.Subset (thickening δ E) (interior (cthickening δ E))

theorem Metric.closure_thickening_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : HasSubset.Subset (closure (thickening δ E)) (cthickening δ E)

theorem Metric.closure_subset_cthickening {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : HasSubset.Subset (closure E) (cthickening δ E)

The closed thickening of a set contains the closure of the set.

theorem Metric.closure_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} (δ_pos : LT.lt 0 δ) (E : Set α) : HasSubset.Subset (closure E) (thickening δ E)

The (open) thickening of a set contains the closure of the set.

theorem Metric.self_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} (δ_pos : LT.lt 0 δ) (E : Set α) : HasSubset.Subset E (thickening δ E)

A set is contained in its own (open) thickening.

theorem Metric.self_subset_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} (E : Set α) : HasSubset.Subset E (cthickening δ E)

A set is contained in its own closed thickening.

theorem Metric.thickening_mem_nhdsSet {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : Real} (hδ : LT.lt 0 δ) : Membership.mem (nhdsSet E) (thickening δ E)

theorem Metric.cthickening_mem_nhdsSet {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : Real} (hδ : LT.lt 0 δ) : Membership.mem (nhdsSet E) (cthickening δ E)

theorem Metric.thickening_union {α : Type u} [PseudoEMetricSpace α] (δ : Real) (s t : Set α) : Eq (thickening δ (Union.union s t)) (Union.union (thickening δ s) (thickening δ t))

theorem Metric.cthickening_union {α : Type u} [PseudoEMetricSpace α] (δ : Real) (s t : Set α) : Eq (cthickening δ (Union.union s t)) (Union.union (cthickening δ s) (cthickening δ t))

theorem Metric.thickening_iUnion {ι : Sort u_1} {α : Type u} [PseudoEMetricSpace α] (δ : Real) (f : ι → Set α) : Eq (thickening δ (Set.iUnion fun (i : ι) => f i)) (Set.iUnion fun (i : ι) => thickening δ (f i))

theorem Metric.thickening_biUnion {α : Type u} [PseudoEMetricSpace α] {ι : Type u_2} (δ : Real) (f : ι → Set α) (I : Set ι) : Eq (thickening δ (Set.iUnion fun (i : ι) => Set.iUnion fun (h : Membership.mem I i) => f i)) (Set.iUnion fun (i : ι) => Set.iUnion fun (h : Membership.mem I i) => thickening δ (f i))

theorem Metric.ediam_cthickening_le {α : Type u} [PseudoEMetricSpace α] {s : Set α} (ε : NNReal) : LE.le (EMetric.diam (cthickening ε.toReal s)) (HAdd.hAdd (EMetric.diam s) (HMul.hMul 2 (ENNReal.ofNNReal ε)))

theorem Metric.ediam_thickening_le {α : Type u} [PseudoEMetricSpace α] {s : Set α} (ε : NNReal) : LE.le (EMetric.diam (thickening ε.toReal s)) (HAdd.hAdd (EMetric.diam s) (HMul.hMul 2 (ENNReal.ofNNReal ε)))

theorem Metric.diam_cthickening_le {ε : Real} {α : Type u_2} [PseudoMetricSpace α] (s : Set α) (hε : LE.le 0 ε) : LE.le (diam (cthickening ε s)) (HAdd.hAdd (diam s) (HMul.hMul 2 ε))

theorem Metric.diam_thickening_le {ε : Real} {α : Type u_2} [PseudoMetricSpace α] (s : Set α) (hε : LE.le 0 ε) : LE.le (diam (thickening ε s)) (HAdd.hAdd (diam s) (HMul.hMul 2 ε))

theorem Metric.thickening_closure {α : Type u} [PseudoEMetricSpace α] {δ : Real} {s : Set α} : Eq (thickening δ (closure s)) (thickening δ s)

theorem Metric.cthickening_closure {α : Type u} [PseudoEMetricSpace α] {δ : Real} {s : Set α} : Eq (cthickening δ (closure s)) (cthickening δ s)

theorem Disjoint.exists_thickenings {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) : Exists fun (δ : Real) => And (LT.lt 0 δ) (Disjoint (Metric.thickening δ s) (Metric.thickening δ t))

theorem Disjoint.exists_cthickenings {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) : Exists fun (δ : Real) => And (LT.lt 0 δ) (Disjoint (Metric.cthickening δ s) (Metric.cthickening δ t))

theorem IsCompact.exists_cthickening_subset_open {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : IsCompact s) (ht : IsOpen t) (hst : HasSubset.Subset s t) : Exists fun (δ : Real) => And (LT.lt 0 δ) (HasSubset.Subset (Metric.cthickening δ s) t)

If s is compact, t is open and s ⊆ t, some cthickening of s is contained in t.

theorem IsCompact.exists_isCompact_cthickening {α : Type u} [PseudoEMetricSpace α] {s : Set α} [LocallyCompactSpace α] (hs : IsCompact s) : Exists fun (δ : Real) => And (LT.lt 0 δ) (IsCompact (Metric.cthickening δ s))

theorem IsCompact.exists_thickening_subset_open {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : IsCompact s) (ht : IsOpen t) (hst : HasSubset.Subset s t) : Exists fun (δ : Real) => And (LT.lt 0 δ) (HasSubset.Subset (Metric.thickening δ s) t)

theorem Metric.hasBasis_nhdsSet_thickening {α : Type u} [PseudoEMetricSpace α] {K : Set α} (hK : IsCompact K) : (nhdsSet K).HasBasis (fun (δ : Real) => LT.lt 0 δ) fun (δ : Real) => thickening δ K

theorem Metric.hasBasis_nhdsSet_cthickening {α : Type u} [PseudoEMetricSpace α] {K : Set α} (hK : IsCompact K) : (nhdsSet K).HasBasis (fun (δ : Real) => LT.lt 0 δ) fun (δ : Real) => cthickening δ K

theorem Metric.cthickening_eq_iInter_cthickening' {α : Type u} [PseudoEMetricSpace α] {δ : Real} (s : Set Real) (hsδ : HasSubset.Subset s (Set.Ioi δ)) (hs : ∀ (ε : Real), LT.lt δ ε → (Inter.inter s (Set.Ioc δ ε)).Nonempty) (E : Set α) : Eq (cthickening δ E) (Set.iInter fun (ε : Real) => Set.iInter fun (h : Membership.mem s ε) => cthickening ε E)

theorem Metric.cthickening_eq_iInter_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} (E : Set α) : Eq (cthickening δ E) (Set.iInter fun (ε : Real) => Set.iInter fun (x : LT.lt δ ε) => cthickening ε E)

theorem Metric.cthickening_eq_iInter_thickening' {α : Type u} [PseudoEMetricSpace α] {δ : Real} (δ_nn : LE.le 0 δ) (s : Set Real) (hsδ : HasSubset.Subset s (Set.Ioi δ)) (hs : ∀ (ε : Real), LT.lt δ ε → (Inter.inter s (Set.Ioc δ ε)).Nonempty) (E : Set α) : Eq (cthickening δ E) (Set.iInter fun (ε : Real) => Set.iInter fun (h : Membership.mem s ε) => thickening ε E)

theorem Metric.cthickening_eq_iInter_thickening {α : Type u} [PseudoEMetricSpace α] {δ : Real} (δ_nn : LE.le 0 δ) (E : Set α) : Eq (cthickening δ E) (Set.iInter fun (ε : Real) => Set.iInter fun (x : LT.lt δ ε) => thickening ε E)

theorem Metric.cthickening_eq_iInter_thickening'' {α : Type u} [PseudoEMetricSpace α] (δ : Real) (E : Set α) : Eq (cthickening δ E) (Set.iInter fun (ε : Real) => Set.iInter fun (x : LT.lt (Max.max 0 δ) ε) => thickening ε E)

theorem Metric.closure_eq_iInter_cthickening' {α : Type u} [PseudoEMetricSpace α] (E : Set α) (s : Set Real) (hs : ∀ (ε : Real), LT.lt 0 ε → (Inter.inter s (Set.Ioc 0 ε)).Nonempty) : Eq (closure E) (Set.iInter fun (δ : Real) => Set.iInter fun (h : Membership.mem s δ) => cthickening δ E)

The closure of a set equals the intersection of its closed thickenings of positive radii accumulating at zero.

theorem Metric.closure_eq_iInter_cthickening {α : Type u} [PseudoEMetricSpace α] (E : Set α) : Eq (closure E) (Set.iInter fun (δ : Real) => Set.iInter fun (x : LT.lt 0 δ) => cthickening δ E)

The closure of a set equals the intersection of its closed thickenings of positive radii.

theorem Metric.closure_eq_iInter_thickening' {α : Type u} [PseudoEMetricSpace α] (E : Set α) (s : Set Real) (hs₀ : HasSubset.Subset s (Set.Ioi 0)) (hs : ∀ (ε : Real), LT.lt 0 ε → (Inter.inter s (Set.Ioc 0 ε)).Nonempty) : Eq (closure E) (Set.iInter fun (δ : Real) => Set.iInter fun (h : Membership.mem s δ) => thickening δ E)

The closure of a set equals the intersection of its open thickenings of positive radii accumulating at zero.

theorem Metric.closure_eq_iInter_thickening {α : Type u} [PseudoEMetricSpace α] (E : Set α) : Eq (closure E) (Set.iInter fun (δ : Real) => Set.iInter fun (x : LT.lt 0 δ) => thickening δ E)

The closure of a set equals the intersection of its (open) thickenings of positive radii.

theorem Metric.frontier_cthickening_subset {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : Real} : HasSubset.Subset (frontier (cthickening δ E)) (setOf fun (x : α) => Eq (EMetric.infEdist x E) (ENNReal.ofReal δ))

The frontier of the closed thickening of a set is contained in an EMetric.infEdist level set.

theorem Metric.closedBall_subset_cthickening {α : Type u_2} [PseudoMetricSpace α] {x : α} {E : Set α} (hx : Membership.mem E x) (δ : Real) : HasSubset.Subset (closedBall x δ) (cthickening δ E)

The closed ball of radius δ centered at a point of E is included in the closed thickening of E.

theorem Metric.cthickening_subset_iUnion_closedBall_of_lt {α : Type u_2} [PseudoMetricSpace α] (E : Set α) {δ δ' : Real} (hδ₀ : LT.lt 0 δ') (hδδ' : LT.lt δ δ') : HasSubset.Subset (cthickening δ E) (Set.iUnion fun (x : α) => Set.iUnion fun (h : Membership.mem E x) => closedBall x δ')

theorem IsCompact.cthickening_eq_biUnion_closedBall {α : Type u_2} [PseudoMetricSpace α] {δ : Real} {E : Set α} (hE : IsCompact E) (hδ : LE.le 0 δ) : Eq (Metric.cthickening δ E) (Set.iUnion fun (x : α) => Set.iUnion fun (h : Membership.mem E x) => Metric.closedBall x δ)

The closed thickening of a compact set E is the union of the balls Metric.closedBall x δ over x ∈ E.

See also Metric.cthickening_eq_biUnion_closedBall.

theorem Metric.cthickening_eq_biUnion_closedBall {δ : Real} {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (E : Set α) (hδ : LE.le 0 δ) : Eq (cthickening δ E) (Set.iUnion fun (x : α) => Set.iUnion fun (h : Membership.mem (closure E) x) => closedBall x δ)

theorem IsClosed.cthickening_eq_biUnion_closedBall {δ : Real} {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {E : Set α} (hE : IsClosed E) (hδ : LE.le 0 δ) : Eq (Metric.cthickening δ E) (Set.iUnion fun (x : α) => Set.iUnion fun (h : Membership.mem E x) => Metric.closedBall x δ)

theorem Metric.infEdist_le_infEdist_cthickening_add {α : Type u} [PseudoEMetricSpace α] {δ : Real} {s : Set α} {x : α} : LE.le (EMetric.infEdist x s) (HAdd.hAdd (EMetric.infEdist x (cthickening δ s)) (ENNReal.ofReal δ))

For the equality, see infEdist_cthickening.

theorem Metric.infEdist_le_infEdist_thickening_add {α : Type u} [PseudoEMetricSpace α] {δ : Real} {s : Set α} {x : α} : LE.le (EMetric.infEdist x s) (HAdd.hAdd (EMetric.infEdist x (thickening δ s)) (ENNReal.ofReal δ))

For the equality, see infEdist_thickening.

theorem Metric.thickening_thickening_subset {α : Type u} [PseudoEMetricSpace α] (ε δ : Real) (s : Set α) : HasSubset.Subset (thickening ε (thickening δ s)) (thickening (HAdd.hAdd ε δ) s)

For the equality, see thickening_thickening.

theorem Metric.thickening_cthickening_subset {α : Type u} [PseudoEMetricSpace α] {δ : Real} (ε : Real) (hδ : LE.le 0 δ) (s : Set α) : HasSubset.Subset (thickening ε (cthickening δ s)) (thickening (HAdd.hAdd ε δ) s)

For the equality, see thickening_cthickening.

theorem Metric.cthickening_thickening_subset {α : Type u} [PseudoEMetricSpace α] {ε : Real} (hε : LE.le 0 ε) (δ : Real) (s : Set α) : HasSubset.Subset (cthickening ε (thickening δ s)) (cthickening (HAdd.hAdd ε δ) s)

For the equality, see cthickening_thickening.

theorem Metric.cthickening_cthickening_subset {α : Type u} [PseudoEMetricSpace α] {δ ε : Real} (hε : LE.le 0 ε) (hδ : LE.le 0 δ) (s : Set α) : HasSubset.Subset (cthickening ε (cthickening δ s)) (cthickening (HAdd.hAdd ε δ) s)

For the equality, see cthickening_cthickening.

theorem Metric.frontier_cthickening_disjoint {α : Type u} [PseudoEMetricSpace α] (A : Set α) : Pairwise (Function.onFun Disjoint fun (r : NNReal) => frontier (cthickening r.toReal A))

theorem Metric.thickening_ball {α : Type u} [PseudoMetricSpace α] (x : α) (ε δ : Real) : HasSubset.Subset (thickening ε (ball x δ)) (ball x (HAdd.hAdd ε δ))

theorem IsCompact.exists_thickening_image_subset {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} [PseudoEMetricSpace β] {f : α → β} {K : Set α} {U : Set β} (hK : IsCompact K) (ho : IsOpen U) (hf : ∀ (x : α), Membership.mem K x → ContinuousAt f x) (hKU : Set.MapsTo f K U) : Exists fun (ε : Real) => And (GT.gt ε 0) (Exists fun (V : Set α) => And (Membership.mem (nhdsSet K) V) (HasSubset.Subset (Metric.thickening ε (Set.image f V)) U))