Collapsing a closed subset to one point

This module constructs the pseudometric on the original space whose metric separation quotient is the quotient used for the injectivity coordinate.

noncomputable def ScottishBook155.collapsedDist {P : Type u} [MetricSpace P] (S : Set P) (x y : P) : ℝ

The distance obtained by allowing a path to jump for free inside S.

Equations

• ScottishBook155.collapsedDist S x y = min (dist x y) (Metric.infDist x S + Metric.infDist y S)

theorem ScottishBook155.collapsedDist_self {P : Type u} [MetricSpace P] (S : Set P) (x : P) : collapsedDist S x x = 0

theorem ScottishBook155.collapsedDist_comm {P : Type u} [MetricSpace P] (S : Set P) (x y : P) : collapsedDist S x y = collapsedDist S y x

theorem ScottishBook155.collapsedDist_triangle {P : Type u} [MetricSpace P] (S : Set P) (x y z : P) : collapsedDist S x z ≤ collapsedDist S x y + collapsedDist S y z

@[implicit_reducible]

noncomputable def ScottishBook155.collapsedPseudoMetricSpace {P : Type u} [MetricSpace P] (S : Set P) : PseudoMetricSpace P

The pseudometric whose separation quotient collapses S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ScottishBook155.CollapsedQuotient (P : Type u) [MetricSpace P] (S : Set P) : Type u

The metric separation quotient of the collapsed pseudometric.

Equations

• ScottishBook155.CollapsedQuotient P S = SeparationQuotient P

@[instance_reducible]

noncomputable instance ScottishBook155.instMetricSpaceCollapsedQuotient {P : Type u} [MetricSpace P] (S : Set P) : MetricSpace (CollapsedQuotient P S)

Equations

• ScottishBook155.instMetricSpaceCollapsedQuotient S = id inferInstance

noncomputable def ScottishBook155.collapseMk {P : Type u} [MetricSpace P] (S : Set P) (x : P) : CollapsedQuotient P S

The canonical map to the collapsed quotient.

Equations

• ScottishBook155.collapseMk S x = id (SeparationQuotient.mk x)

theorem ScottishBook155.dist_collapseMk {P : Type u} [MetricSpace P] (S : Set P) (x y : P) : dist (collapseMk S x) (collapseMk S y) = collapsedDist S x y

theorem ScottishBook155.collapseMk_dist_le {P : Type u} [MetricSpace P] (S : Set P) (x y : P) : dist (collapseMk S x) (collapseMk S y) ≤ dist x y

theorem ScottishBook155.collapseMk_eq_of_mem {P : Type u} [MetricSpace P] {S : Set P} {x y : P} (hx : x ∈ S) (hy : y ∈ S) : collapseMk S x = collapseMk S y

theorem ScottishBook155.collapseMk_injOn_compl {P : Type u} [MetricSpace P] {S : Set P} (hne : S.Nonempty) (hclosed : IsClosed S) : Set.InjOn (collapseMk S) Sᶜ

For a nonempty closed set, the quotient map remains injective away from the collapsed set.

theorem ScottishBook155.collapsedDist_eq_zero_iff {P : Type u} [MetricSpace P] {S : Set P} (hne : S.Nonempty) (hclosed : IsClosed S) (x y : P) : collapsedDist S x y = 0 ↔ x = y ∨ x ∈ S ∧ y ∈ S

theorem ScottishBook155.collapseMk_eq_iff {P : Type u} [MetricSpace P] {S : Set P} (hne : S.Nonempty) (hclosed : IsClosed S) (x y : P) : collapseMk S x = collapseMk S y ↔ x = y ∨ x ∈ S ∧ y ∈ S

noncomputable def ScottishBook155.quotientKuratowski {P : Type u} [MetricSpace P] (S : Set P) (base x : P) : ↥(lp (fun (x : CollapsedQuotient P S) => ℝ) ⊤)

The manuscript's injectivity coordinate, represented in unrestricted ℓ∞ after collapsing S.

Equations

• ScottishBook155.quotientKuratowski S base x = ScottishBook155.fullKuratowski (ScottishBook155.collapseMk S base) (ScottishBook155.collapseMk S x)

theorem ScottishBook155.quotientKuratowski_of_mem {P : Type u} [MetricSpace P] {S : Set P} {base x : P} (hbase : base ∈ S) (hx : x ∈ S) : quotientKuratowski S base x = 0

theorem ScottishBook155.quotientKuratowski_dist_le {P : Type u} [MetricSpace P] (S : Set P) (base x y : P) : dist (quotientKuratowski S base x) (quotientKuratowski S base y) ≤ dist x y

theorem ScottishBook155.quotientKuratowski_eq_iff {P : Type u} [MetricSpace P] {S : Set P} (hne : S.Nonempty) (hclosed : IsClosed S) (base x y : P) : quotientKuratowski S base x = quotientKuratowski S base y ↔ x = y ∨ x ∈ S ∧ y ∈ S