Metric.toInductiveLimit_commute
theorem Metric.toInductiveLimit_commute :
∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)}
(I : ∀ (n : ℕ), Isometry (f n)) (n : ℕ), Metric.toInductiveLimit I n.succ ∘ f n = Metric.toInductiveLimit I n
The theorem `Metric.toInductiveLimit_commute` states that for any sequence of types `X` indexed by natural numbers (where each type `X n` is a metric space), and a sequence of mappings `f` (where each mapping `f n` is an isometry from `X n` to `X (n+1)`), the function composition of `toInductiveLimit` for `n.succ` (i.e., `n+1`) after `f n` is the same as `toInductiveLimit` for `n`. In other words, the mappings to the inductive limit are consistent with the mappings `f n` that transitively connect the spaces `X n` and `X (n+1)`. This ensures the coherence of the inductive limit in the context of metric spaces, and allows us to make meaningful comparisons across different levels of the sequence.
More concisely: Given a sequence of metric spaces `(X : ℕ → Type)` and isometries `(f : ∀n, X n → X ( suc n )`, the induced maps on inductive limits `(toInductiveLimit X : Type) ≅ (toInductiveLimit X '' suc) ∘ f` hold true.
|
Metric.toInductiveLimit_isometry
theorem Metric.toInductiveLimit_isometry :
∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)}
(I : ∀ (n : ℕ), Isometry (f n)) (n : ℕ), Isometry (Metric.toInductiveLimit I n)
The theorem `Metric.toInductiveLimit_isometry` states that for any sequence of metric spaces `X n` and a sequence of mappings `f n` from `X n` to `X (n + 1)`, where each `f n` is an isometry, the map `toInductiveLimit n` that sends each `X n` to the inductive limit of this sequence of metric spaces is an isometry. An isometry is a function that preserves the distance between any pair of points in these metric spaces.
More concisely: The inductive limit of a sequence of metric spaces and isometries between them is an isometry.
|
Metric.inductiveLimitDist.proof_1
theorem Metric.inductiveLimitDist.proof_1 : ∀ {X : ℕ → Type u_1} (x y : (n : ℕ) × X n), x.fst ≤ max x.fst y.fst := by
sorry
This theorem states that for any function `X` from natural numbers to some type `u_1`, and any two ordered pairs `x` and `y` where each pair consists of a natural number and an element of the type at that natural number, the natural number in pair `x` is less than or equal to the maximum of the natural numbers in pairs `x` and `y`. In mathematical terms, for all `x, y` in the product set of natural numbers and `X n`, `x.fst` is less than or equal to the maximum of `x.fst` and `y.fst`.
More concisely: For all functions `X` from natural numbers to some type `u_1` and all pairs `x` and `y` in the product set of natural numbers and `X` where `x.1` and `y.1` are natural numbers, `x.1` ≤ max `x.1` and `y.1`.
|
Metric.isometry_inr
theorem Metric.isometry_inr :
∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y], Isometry Sum.inr
This theorem states that the function that injects a space into the right-hand side of a disjoint union is an isometry. In other words, for any two types `X` and `Y` that are metric spaces, the function `Sum.inr` (which maps any element of `Y` to the corresponding element of `X + Y`, the disjoint union of `X` and `Y`) preserves the distance between elements. Specifically, for any two elements `y1` and `y2` in `Y`, the distance between `Sum.inr y1` and `Sum.inr y2` in the disjoint union is the same as the distance between `y1` and `y2` in `Y`.
More concisely: The function `Sum.inr : Y → X + Y` is an isometry between the metric spaces `Y` and `X + Y`, preserving the distance between any two elements in `Y`.
|
Metric.inductiveLimitDist_eq_dist
theorem Metric.inductiveLimitDist_eq_dist :
∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)},
(∀ (n : ℕ), Isometry (f n)) →
∀ (x y : (n : ℕ) × X n) (m : ℕ) (hx : x.fst ≤ m) (hy : y.fst ≤ m),
Metric.inductiveLimitDist f x y =
dist (Nat.leRecOn hx (fun {k} => f k) x.snd) (Nat.leRecOn hy (fun {k} => f k) y.snd)
The theorem `Metric.inductiveLimitDist_eq_dist` states that for any sequence of types `X` indexed by natural numbers, where each `X n` is a metric space, and for any function `f` that maps elements of `X n` to `X (n + 1)` and preserves distances (isometry), the pre-distance on the disjoint union of all `X n` (calculated by the `Metric.inductiveLimitDist` function) can be computed in any `X k` for large enough `k`. More specifically, given any two elements `x` and `y` from the disjoint union and any natural number `m` such that the indices of `x` and `y` are less than or equal to `m`, the pre-distance between `x` and `y` is equal to the distance between the images of `x` and `y` under the function `f` recursively applied `m` times.
More concisely: For any isometry `f` between metric spaces `X n` indexed by natural numbers, the pre-distance in the inductive limit of `X` equals the distance between the images of elements under recursive application of `f`.
|
Metric.Sigma.isometry_mk
theorem Metric.Sigma.isometry_mk :
∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (i : ι), Isometry (Sigma.mk i)
This theorem states that for a given type `ι` and a function `E` that maps from `ι` to another type, assuming every `E i` forms a metric space for every `i` in `ι`, the function that maps any element in `ι` to a corresponding disjoint union (using the `Sigma.mk i` function) is an isometry. In other words, this function preserves the distances between all pairs of elements in the space.
More concisely: Given a type `ι` and a function `E : ι → X` where each `E i` forms a metric space, the function `Σ i, i : ι → E i → *` is an isometry.
|
Metric.Sigma.completeSpace
theorem Metric.Sigma.completeSpace :
∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] [inst_1 : ∀ (i : ι), CompleteSpace (E i)],
CompleteSpace ((i : ι) × E i)
This theorem states that for any type `ι` and a function `E` from `ι` to some type, if each `E i` is a complete metric space for every `i` in `ι`, then the disjoint union, represented as a tuple `(i : ι, E i)`, is also a complete metric space. In other words, the theorem asserts that the disjoint union of complete metric spaces is itself a complete metric space.
More concisely: Given a type `ι` and a family `{E i : _ | i ∈ ι}` of complete metric spaces indexed by `ι`, the disjoint union `{(i, x) | i ∈ ι, x ∈ E i}` is a complete metric space.
|
Metric.isometry_inl
theorem Metric.isometry_inl :
∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y], Isometry Sum.inl
This theorem states that the left injection of a space into a disjoint union is an isometry. More specifically, for any two types `X` and `Y` that are both metric spaces, the left injection function `Sum.inl`, which maps an element of `X` to an element of the disjoint union of `X` and `Y`, preserves the metric distance. In other words, the distance between any two points in `X` is the same as the distance between their images in the disjoint union when mapped by the `Sum.inl` function.
More concisely: The left injection function from a metric space `X` into the disjoint union of `X` and `Y` is an isometry.
|