The source-side metric-adjunction formula #
The asymmetric adjunction in the manuscript glues a closed subset of the
source to the old target by a nonexpansive map. Mathlib's exact metric gluing
requires two isometric maps, so it does not directly apply. Here we formalize
the source--source distance candidate from the manuscript and prove its key
short-scale property: an excursion through the old target cannot shorten a
source pair of distance at most r.
noncomputable def
ScottishBook155.attachmentExcursionCost
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
Length of the cheapest source--target--source excursion in the proposed metric adjunction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ScottishBook155.sourceAdjunctionDist
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
The manuscript's source--source adjunction distance formula, before the ambient quotient space is constructed.
Equations
- ScottishBook155.sourceAdjunctionDist V a y H x₀ x₁ = min (dist x₀ x₁) (ScottishBook155.attachmentExcursionCost V a y H x₀ x₁)
Instances For
noncomputable def
ScottishBook155.attachmentTargetCost
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x : OneSum M)
(n : N)
:
Distance candidate from a source point to an old-target point.
Equations
- ScottishBook155.attachmentTargetCost V a y H x n = ⨅ (p : M ⊕ Unit), dist x (ScottishBook155.attachmentPoint a H p) + dist (ScottishBook155.attachmentMap V y p) n
Instances For
noncomputable def
ScottishBook155.adjunctionPreDist
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
:
The two-layer adjunction predistance on the disjoint union of the source and old target. The remaining construction step is to prove its triangle inequality and take its metric separation quotient.
Equations
- ScottishBook155.adjunctionPreDist V a y H (Sum.inl x₀) (Sum.inl x₁) = ScottishBook155.sourceAdjunctionDist V a y H x₀ x₁
- ScottishBook155.adjunctionPreDist V a y H (Sum.inr n₀) (Sum.inr n₁) = dist n₀ n₁
- ScottishBook155.adjunctionPreDist V a y H (Sum.inl x_2) (Sum.inr n) = ScottishBook155.attachmentTargetCost V a y H x_2 n
- ScottishBook155.adjunctionPreDist V a y H (Sum.inr n) (Sum.inl x_2) = ScottishBook155.attachmentTargetCost V a y H x_2 n
Instances For
theorem
ScottishBook155.attachmentTargetCost_nonneg
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x : OneSum M)
(n : N)
:
theorem
ScottishBook155.attachmentTargetCost_le
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x : OneSum M)
(n : N)
(p : M ⊕ Unit)
:
theorem
ScottishBook155.infDist_attachmentSet_le_attachmentTargetCost
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x : OneSum M)
(n : N)
:
theorem
ScottishBook155.attachmentTargetCost_eq_collar
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{N : Type v}
[PseudoMetricSpace N]
{V : M → N}
{a : M}
{y : N}
{H r : ℝ}
(hr : 0 < r)
(hH : 2 * r + dist (V a) y < H)
(hshort : PreservesUpTo r V)
(m : M)
{s : ℝ}
(hs : |s| < r)
(n : N)
:
Inside the protected vertical collar, the source--target adjunction cost is exactly the vertical distance to the base plus the old-target distance from the image of the horizontal coordinate.
theorem
ScottishBook155.attachmentExcursionCost_nonneg
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
theorem
ScottishBook155.attachmentExcursionCost_le
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
(p q : M ⊕ Unit)
:
attachmentExcursionCost V a y H x₀ x₁ ≤ dist x₀ (attachmentPoint a H p) + dist (attachmentMap V y p) (attachmentMap V y q) + dist (attachmentPoint a H q) x₁
theorem
ScottishBook155.attachmentExcursionCost_comm
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
theorem
ScottishBook155.infDist_attachmentSet_le_excursionCost_left
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
theorem
ScottishBook155.infDist_attachmentSet_le_excursionCost_right
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
theorem
ScottishBook155.dist_attachmentMap_le_excursionCost
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[MetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(p q : M ⊕ Unit)
:
dist (attachmentMap V y p) (attachmentMap V y q) ≤ attachmentExcursionCost V a y H (attachmentPoint a H p) (attachmentPoint a H q)
theorem
ScottishBook155.eq_of_attachmentExcursionCost_eq_zero
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[MetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(hinj : Function.Injective (attachmentMap V y))
{x₀ x₁ : OneSum M}
(hzero : attachmentExcursionCost V a y H x₀ x₁ = 0)
:
Zero excursion cost forces equal source points when the prescribed attachment map is injective.
theorem
ScottishBook155.eq_of_sourceAdjunctionDist_eq_zero
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[MetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(hinj : Function.Injective (attachmentMap V y))
{x₀ x₁ : OneSum M}
(hzero : sourceAdjunctionDist V a y H x₀ x₁ = 0)
:
theorem
ScottishBook155.sourceAdjunctionDist_comm
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
theorem
ScottishBook155.sourceAdjunctionDist_le_excursion
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
(p q : M ⊕ Unit)
:
sourceAdjunctionDist V a y H x₀ x₁ ≤ dist x₀ (attachmentPoint a H p) + dist (attachmentMap V y p) (attachmentMap V y q) + dist (attachmentPoint a H q) x₁
theorem
ScottishBook155.attachmentTargetCost_triangle_target
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x : OneSum M)
(n₀ n₁ : N)
:
One mixed triangle inequality: moving inside the old target after entering it cannot make the source--target cost larger than the corresponding sum.
theorem
ScottishBook155.sourceAdjunctionDist_triangle_target
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
(n : N)
:
sourceAdjunctionDist V a y H x₀ x₁ ≤ attachmentTargetCost V a y H x₀ n + attachmentTargetCost V a y H x₁ n
A target point may serve as the middle vertex of a source--source triangle.
theorem
ScottishBook155.dist_triangle_attachmentTargetCost
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(n₀ n₁ : N)
(x : OneSum M)
:
If the attachment map is nonexpansive, a source point may serve as the middle vertex of an old-target triangle.
theorem
ScottishBook155.adjunctionPreDist_triangle_middle_target
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(z₀ z₁ : OneSum M ⊕ N)
(n : N)
:
adjunctionPreDist V a y H z₀ z₁ ≤ adjunctionPreDist V a y H z₀ (Sum.inr n) + adjunctionPreDist V a y H (Sum.inr n) z₁
theorem
ScottishBook155.attachmentTargetCost_triangle_source
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(x₀ x₁ : OneSum M)
(n : N)
:
attachmentTargetCost V a y H x₀ n ≤ sourceAdjunctionDist V a y H x₀ x₁ + attachmentTargetCost V a y H x₁ n
Mixed triangle inequality with a source point in the middle. The proof splits according to which branch of the source--source minimum is active.
theorem
ScottishBook155.adjunctionPreDist_triangle_target_source_target
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(n₀ n₁ : N)
(x : OneSum M)
:
adjunctionPreDist V a y H (Sum.inr n₀) (Sum.inr n₁) ≤ adjunctionPreDist V a y H (Sum.inr n₀) (Sum.inl x) + adjunctionPreDist V a y H (Sum.inl x) (Sum.inr n₁)
theorem
ScottishBook155.adjunctionPreDist_triangle_source_source_target
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(x₀ x₁ : OneSum M)
(n : N)
:
adjunctionPreDist V a y H (Sum.inl x₀) (Sum.inr n) ≤ adjunctionPreDist V a y H (Sum.inl x₀) (Sum.inl x₁) + adjunctionPreDist V a y H (Sum.inl x₁) (Sum.inr n)
theorem
ScottishBook155.sourceAdjunctionDist_triangle_direct_left
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ x₂ : OneSum M)
:
theorem
ScottishBook155.sourceAdjunctionDist_triangle_direct_right
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ x₂ : OneSum M)
:
theorem
ScottishBook155.sourceAdjunctionDist_triangle
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(x₀ x₁ x₂ : OneSum M)
:
sourceAdjunctionDist V a y H x₀ x₂ ≤ sourceAdjunctionDist V a y H x₀ x₁ + sourceAdjunctionDist V a y H x₁ x₂
theorem
ScottishBook155.sourceAdjunctionDist_self
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x : OneSum M)
:
theorem
ScottishBook155.adjunctionPreDist_self
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(z : OneSum M ⊕ N)
:
theorem
ScottishBook155.adjunctionPreDist_comm
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(z₀ z₁ : OneSum M ⊕ N)
:
theorem
ScottishBook155.adjunctionPreDist_triangle
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(z₀ z₁ z₂ : OneSum M ⊕ N)
:
@[implicit_reducible]
noncomputable def
ScottishBook155.adjunctionPseudoMetricSpace
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
PseudoMetricSpace (OneSum M ⊕ N)
The gluing pseudometric on the disjoint union of the one-sum source and target, under the attachment distance bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ScottishBook155.attachmentTargetCost_glued
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(p : M ⊕ Unit)
:
theorem
ScottishBook155.adjunctionPreDist_glued
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(p : M ⊕ Unit)
:
theorem
ScottishBook155.adjunctionPreDist_target
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(n₀ n₁ : N)
:
theorem
ScottishBook155.sourceAdjunctionDist_le
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(x₀ x₁ : OneSum M)
:
theorem
ScottishBook155.dist_le_attachmentExcursionCost_of_short
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{N : Type v}
[PseudoMetricSpace N]
{V : M → N}
{a : M}
{y : N}
{H r : ℝ}
(hr : 0 < r)
(hH : 2 * r < H)
(hshort : PreservesUpTo r V)
{x₀ x₁ : OneSum M}
(hd : dist x₀ x₁ ≤ r)
:
For a short source pair, every excursion through the attachment set and the old target has length at least the original source distance.
theorem
ScottishBook155.sourceAdjunctionDist_eq_of_short
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{N : Type v}
[PseudoMetricSpace N]
{V : M → N}
{a : M}
{y : N}
{H r : ℝ}
(hr : 0 < r)
(hH : 2 * r < H)
(hshort : PreservesUpTo r V)
{x₀ x₁ : OneSum M}
(hd : dist x₀ x₁ ≤ r)
:
The source-side adjunction formula preserves every distance at most r.
theorem
ScottishBook155.adjunctionPreDist_source_eq_of_short
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{N : Type v}
[PseudoMetricSpace N]
{V : M → N}
{a : M}
{y : N}
{H r : ℝ}
(hr : 0 < r)
(hH : 2 * r < H)
(hshort : PreservesUpTo r V)
{x₀ x₁ : OneSum M}
(hd : dist x₀ x₁ ≤ r)
:
noncomputable def
ScottishBook155.AdjunctionSpace
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
Type (max u v)
The metric separation quotient realizing the asymmetric metric adjunction.
Equations
- ScottishBook155.AdjunctionSpace V a y H hattach = SeparationQuotient (ScottishBook155.OneSum M ⊕ N)
Instances For
@[instance_reducible]
noncomputable instance
ScottishBook155.instMetricSpaceAdjunctionSpace
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
MetricSpace (AdjunctionSpace V a y H hattach)
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
ScottishBook155.adjunctionSourceMk
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(x : OneSum M)
:
AdjunctionSpace V a y H hattach
The canonical map from the one-sum source into the metric adjunction space.
Equations
- ScottishBook155.adjunctionSourceMk V a y H hattach x = Quotient.mk'' (Sum.inl x)
Instances For
instance
ScottishBook155.adjunctionSpaceNonempty
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
Nonempty (AdjunctionSpace V a y H hattach)
noncomputable def
ScottishBook155.adjunctionTargetMk
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(n : N)
:
AdjunctionSpace V a y H hattach
The canonical map from the target into the metric adjunction space.
Equations
- ScottishBook155.adjunctionTargetMk V a y H hattach n = Quotient.mk'' (Sum.inr n)
Instances For
theorem
ScottishBook155.dist_adjunctionTargetMk
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(n₀ n₁ : N)
:
theorem
ScottishBook155.dist_adjunctionSourceMk_targetMk_eq_collar
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{N : Type v}
[PseudoMetricSpace N]
{V : M → N}
{a : M}
{y : N}
{H r : ℝ}
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(hr : 0 < r)
(hH : 2 * r + dist (V a) y < H)
(hshort : PreservesUpTo r V)
(m : M)
{s : ℝ}
(hs : |s| < r)
(n : N)
:
dist (adjunctionSourceMk V a y H hattach (WithLp.toLp 1 (m, s))) (adjunctionTargetMk V a y H hattach n) = |s| + dist (V m) n
theorem
ScottishBook155.adjunctionTargetMk_isometry
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
:
Isometry (adjunctionTargetMk V a y H hattach)
theorem
ScottishBook155.adjunctionMk_glued
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(p : M ⊕ Unit)
:
adjunctionSourceMk V a y H hattach (attachmentPoint a H p) = adjunctionTargetMk V a y H hattach (attachmentMap V y p)
theorem
ScottishBook155.infDist_adjunctionTarget_range_eq_attachmentSet
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[PseudoMetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(x : OneSum M)
:
Metric.infDist (adjunctionSourceMk V a y H hattach x) (Set.range (adjunctionTargetMk V a y H hattach)) = Metric.infDist x (attachmentSet a H)
Distance from a source point to the embedded old target is exactly its distance to the source attachment set.
theorem
ScottishBook155.dist_adjunctionSourceMk_of_short
{M : Type u}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
{N : Type v}
[PseudoMetricSpace N]
{V : M → N}
{a : M}
{y : N}
{H r : ℝ}
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(hr : 0 < r)
(hH : 2 * r < H)
(hshort : PreservesUpTo r V)
{x₀ x₁ : OneSum M}
(hd : dist x₀ x₁ ≤ r)
:
theorem
ScottishBook155.adjunctionSourceMk_injective
{M : Type u}
[NormedAddCommGroup M]
{N : Type v}
[MetricSpace N]
(V : M → N)
(a : M)
(y : N)
(H : ℝ)
(hattach :
∀ (p q : M ⊕ Unit),
dist (attachmentMap V y p) (attachmentMap V y q) ≤ dist (attachmentPoint a H p) (attachmentPoint a H q))
(hinj : Function.Injective (attachmentMap V y))
:
Function.Injective (adjunctionSourceMk V a y H hattach)