Documentation

Mathlib.Topology.MetricSpace.Thickening

Thickenings in pseudo-metric spaces #

Main definitions #

Main results #

def Metric.thickening {α : Type u} [PseudoEMetricSpace α] (δ : ) (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
Instances For
    theorem Metric.eventually_not_mem_thickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : xclosure E) :
    ∀ᶠ (δ : ) in nhds 0, xMetric.thickening δ E

    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 δ.

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

    theorem Metric.isOpen_thickening {α : Type u} [PseudoEMetricSpace α] {δ : } {E : Set α} :

    The (open) thickening is an open set.

    @[simp]

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

    theorem Metric.thickening_of_nonpos {α : Type u} [PseudoEMetricSpace α] {δ : } (hδ : δ 0) (s : Set α) :
    theorem Metric.thickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :

    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 α] (δ : ) {E₁ : Set α} {E₂ : Set α} (h : E₁ 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 α] {δ : } (E : Set α) (x : α) :
    x Metric.thickening δ E zE, edist x z < 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 (Disjoint on fun (r : ) => frontier (Metric.thickening r A))

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

    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 {δ : } {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} (h : E.Nonempty) :
    theorem Metric.mem_thickening_iff {δ : } {X : Type u} [PseudoMetricSpace X] {E : Set X} {x : X} :
    x Metric.thickening δ E zE, 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.

    @[simp]
    theorem Metric.thickening_singleton {X : Type u} [PseudoMetricSpace X] (δ : ) (x : X) :
    theorem Metric.ball_subset_thickening {X : Type u} [PseudoMetricSpace X] {x : X} {E : Set X} (hx : x E) (δ : ) :
    theorem Metric.thickening_eq_biUnion_ball {X : Type u} [PseudoMetricSpace X] {δ : } {E : Set X} :
    Metric.thickening δ E = xE, Metric.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.

    def Metric.cthickening {α : Type u} [PseudoEMetricSpace α] (δ : ) (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
    Instances For
      @[simp]
      theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos {α : Type u} [PseudoEMetricSpace α] {E : Set α} {x : α} (h : xclosure E) :
      ∀ᶠ (δ : ) in nhds 0, xMetric.cthickening δ E

      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 : α) (δ : ) (E : Set α) (h : y E) (h' : edist x y ENNReal.ofReal δ) :
      theorem Metric.mem_cthickening_of_dist_le {α : Type u_2} [PseudoMetricSpace α] (x : α) (y : α) (δ : ) (E : Set α) (h : y E) (h' : dist x y δ) :

      The closed thickening is a closed set.

      @[simp]

      The closed thickening of the empty set is empty.

      theorem Metric.cthickening_of_nonpos {α : Type u} [PseudoEMetricSpace α] {δ : } (hδ : δ 0) (E : Set α) :
      @[simp]

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

      theorem Metric.cthickening_mono {α : Type u} [PseudoEMetricSpace α] {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :

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

      @[simp]
      theorem Metric.cthickening_singleton {α : Type u_2} [PseudoMetricSpace α] (x : α) {δ : } (hδ : 0 δ) :
      theorem Metric.cthickening_subset_of_subset {α : Type u} [PseudoEMetricSpace α] (δ : ) {E₁ : Set α} {E₂ : Set α} (h : E₁ 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} {δ₂ : } (hlt : δ₁ < δ₂) (E : Set α) :
      theorem Metric.cthickening_subset_thickening' {α : Type u} [PseudoEMetricSpace α] {δ₁ : } {δ₂ : } (δ₂_pos : 0 < δ₂) (hlt : δ₁ < δ₂) (E : Set α) :

      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.

      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 α] {δ₁ : } {δ₂ : } (hle : δ₁ δ₂) (E : Set α) :
      theorem IsCompact.cthickening {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {s : Set α} (hs : IsCompact s) {r : } :

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

      theorem Metric.closure_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ : } (δ_pos : 0 < δ) (E : Set α) :

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

      theorem Metric.self_subset_thickening {α : Type u} [PseudoEMetricSpace α] {δ : } (δ_pos : 0 < δ) (E : Set α) :

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

      A set is contained in its own closed thickening.

      theorem Metric.thickening_mem_nhdsSet {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : } (hδ : 0 < δ) :
      theorem Metric.cthickening_mem_nhdsSet {α : Type u} [PseudoEMetricSpace α] (E : Set α) {δ : } (hδ : 0 < δ) :
      @[simp]
      theorem Metric.thickening_union {α : Type u} [PseudoEMetricSpace α] (δ : ) (s : Set α) (t : Set α) :
      @[simp]
      theorem Metric.cthickening_union {α : Type u} [PseudoEMetricSpace α] (δ : ) (s : Set α) (t : Set α) :
      @[simp]
      theorem Metric.thickening_iUnion {ι : Sort u_1} {α : Type u} [PseudoEMetricSpace α] (δ : ) (f : ιSet α) :
      Metric.thickening δ (⋃ (i : ι), f i) = ⋃ (i : ι), Metric.thickening δ (f i)
      theorem Metric.thickening_biUnion {α : Type u} [PseudoEMetricSpace α] {ι : Type u_2} (δ : ) (f : ιSet α) (I : Set ι) :
      Metric.thickening δ (⋃ iI, f i) = iI, Metric.thickening δ (f i)
      theorem Metric.diam_cthickening_le {ε : } {α : Type u_2} [PseudoMetricSpace α] (s : Set α) (hε : 0 ε) :
      theorem Metric.diam_thickening_le {ε : } {α : Type u_2} [PseudoMetricSpace α] (s : Set α) (hε : 0 ε) :
      theorem Disjoint.exists_thickenings {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) :
      ∃ (δ : ), 0 < δ Disjoint (Metric.thickening δ s) (Metric.thickening δ t)
      theorem Disjoint.exists_cthickenings {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) :
      ∃ (δ : ), 0 < δ Disjoint (Metric.cthickening δ s) (Metric.cthickening δ t)
      theorem IsCompact.exists_cthickening_subset_open {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsOpen t) (hst : s t) :
      ∃ (δ : ), 0 < δ 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_thickening_subset_open {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsOpen t) (hst : s t) :
      ∃ (δ : ), 0 < δ Metric.thickening δ s t
      theorem Metric.hasBasis_nhdsSet_thickening {α : Type u} [PseudoEMetricSpace α] {K : Set α} (hK : IsCompact K) :
      (nhdsSet K).HasBasis (fun (δ : ) => 0 < δ) fun (δ : ) => Metric.thickening δ K
      theorem Metric.hasBasis_nhdsSet_cthickening {α : Type u} [PseudoEMetricSpace α] {K : Set α} (hK : IsCompact K) :
      (nhdsSet K).HasBasis (fun (δ : ) => 0 < δ) fun (δ : ) => Metric.cthickening δ K
      theorem Metric.cthickening_eq_iInter_cthickening' {α : Type u} [PseudoEMetricSpace α] {δ : } (s : Set ) (hsδ : s Set.Ioi δ) (hs : ∀ (ε : ), δ < ε(s Set.Ioc δ ε).Nonempty) (E : Set α) :
      Metric.cthickening δ E = εs, Metric.cthickening ε E
      theorem Metric.cthickening_eq_iInter_cthickening {α : Type u} [PseudoEMetricSpace α] {δ : } (E : Set α) :
      Metric.cthickening δ E = ⋂ (ε : ), ⋂ (_ : δ < ε), Metric.cthickening ε E
      theorem Metric.cthickening_eq_iInter_thickening' {α : Type u} [PseudoEMetricSpace α] {δ : } (δ_nn : 0 δ) (s : Set ) (hsδ : s Set.Ioi δ) (hs : ∀ (ε : ), δ < ε(s Set.Ioc δ ε).Nonempty) (E : Set α) :
      Metric.cthickening δ E = εs, Metric.thickening ε E
      theorem Metric.cthickening_eq_iInter_thickening {α : Type u} [PseudoEMetricSpace α] {δ : } (δ_nn : 0 δ) (E : Set α) :
      Metric.cthickening δ E = ⋂ (ε : ), ⋂ (_ : δ < ε), Metric.thickening ε E
      theorem Metric.cthickening_eq_iInter_thickening'' {α : Type u} [PseudoEMetricSpace α] (δ : ) (E : Set α) :
      Metric.cthickening δ E = ⋂ (ε : ), ⋂ (_ : max 0 δ < ε), Metric.thickening ε E
      theorem Metric.closure_eq_iInter_cthickening' {α : Type u} [PseudoEMetricSpace α] (E : Set α) (s : Set ) (hs : ∀ (ε : ), 0 < ε(s Set.Ioc 0 ε).Nonempty) :
      closure E = δs, Metric.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 α) :
      closure E = ⋂ (δ : ), ⋂ (_ : 0 < δ), Metric.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 ) (hs₀ : s Set.Ioi 0) (hs : ∀ (ε : ), 0 < ε(s Set.Ioc 0 ε).Nonempty) :
      closure E = δs, Metric.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 α) :
      closure E = ⋂ (δ : ), ⋂ (_ : 0 < δ), Metric.thickening δ E

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

      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 : x 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 α) {δ : } {δ' : } (hδ₀ : 0 < δ') (hδδ' : δ < δ') :
      Metric.cthickening δ E xE, Metric.closedBall x δ'
      theorem IsCompact.cthickening_eq_biUnion_closedBall {α : Type u_2} [PseudoMetricSpace α] {δ : } {E : Set α} (hE : IsCompact E) (hδ : 0 δ) :
      Metric.cthickening δ E = xE, 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 {δ : } {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] (E : Set α) (hδ : 0 δ) :
      theorem IsClosed.cthickening_eq_biUnion_closedBall {δ : } {α : Type u_2} [PseudoMetricSpace α] [ProperSpace α] {E : Set α} (hE : IsClosed E) (hδ : 0 δ) :
      Metric.cthickening δ E = xE, Metric.closedBall x δ

      For the equality, see infEdist_cthickening.

      For the equality, see infEdist_thickening.

      @[simp]

      For the equality, see thickening_thickening.

      @[simp]
      theorem Metric.thickening_cthickening_subset {α : Type u} [PseudoEMetricSpace α] {δ : } (ε : ) (hδ : 0 δ) (s : Set α) :

      For the equality, see thickening_cthickening.

      @[simp]
      theorem Metric.cthickening_thickening_subset {α : Type u} [PseudoEMetricSpace α] {ε : } (hε : 0 ε) (δ : ) (s : Set α) :

      For the equality, see cthickening_thickening.

      @[simp]
      theorem Metric.cthickening_cthickening_subset {α : Type u} [PseudoEMetricSpace α] {δ : } {ε : } (hε : 0 ε) (hδ : 0 δ) (s : Set α) :

      For the equality, see cthickening_cthickening.

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