PiNat.apply_firstDiff_ne
theorem PiNat.apply_firstDiff_ne :
∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n}, x ≠ y → x (PiNat.firstDiff x y) ≠ y (PiNat.firstDiff x y)
This theorem states that for any function `E` that maps natural numbers to a certain type, and any two functions `x` and `y` (that are both of type `E`), if `x` and `y` are not equal, then the values of `x` and `y` at the first index at which they differ (given by `PiNat.firstDiff x y`) are also not equal. In other words, it asserts that if two such functions are not the same, they must differ at least at one index.
More concisely: For any function `E` mapping natural numbers to a type and two distinct functions `x` and `y` of type `E`, `PiNat.firstDiff x y` is also distinct.
|
PiNat.dist_eq_of_ne
theorem PiNat.dist_eq_of_ne :
∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n}, x ≠ y → dist x y = (1 / 2) ^ PiNat.firstDiff x y
This theorem states that for any function `E` from natural numbers to some type `u_1`, and for any two functions `x` and `y` from natural numbers to `E`, if `x` and `y` are not equal, then the distance between `x` and `y` (using the distance metric in the product space `Π n, E n`) is equal to `(1 / 2)` raised to the power of the first index at which `x` and `y` differ (`PiNat.firstDiff x y`). Here, `PiNat.firstDiff x y` is defined as the first natural number `n` for which `x(n)` and `y(n)` are distinct.
More concisely: For any function `E : Nat → Type_, and functions `x, y : Nat → E`, if `x ≠ y`, then the distance between `x` and `y` in the product space `Π n, E n` is equal to `(1 / 2) ^ (PiNat.firstDiff x y)`.
|
PiNat.mem_cylinder_comm
theorem PiNat.mem_cylinder_comm :
∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) (n : ℕ), y ∈ PiNat.cylinder x n ↔ x ∈ PiNat.cylinder y n
This theorem states that, for any given function `E` from natural numbers to some types, and any two sequences `x` and `y` in the product space of `E`, along with a natural number `n`, the sequence `y` is in the `n`-length cylinder set around `x` if and only if the sequence `x` is in the `n`-length cylinder set around `y`. In other words, `y` coincides with `x` for the first `n` terms if and only if `x` coincides with `y` for the first `n` terms.
More concisely: For any function `E` from natural numbers to types and sequences `x` and `y` in the product space of `E^N`, where `N` is the natural numbers, the sequences `x` and `y` belong to each other's `n`-length cylinder sets if and only if they coincide for the first `n` terms.
|
PiNat.dist_triangle
theorem PiNat.dist_triangle : ∀ {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n), dist x z ≤ dist x y + dist y z
This theorem is a formalization of the triangle inequality in the context of Pi types over natural numbers in Lean 4. Given three functions `x`, `y`, and `z` from natural numbers to some type `E`, the theorem states that the distance between `x` and `z` is less than or equal to the sum of the distance between `x` and `y` and the distance between `y` and `z`. Here, the `dist` function measures some notion of distance between two functions of the same type. This is a generalization of the triangle inequality from metric spaces to this specific context.
More concisely: Given functions `x`, `y`, and `z` from natural numbers to some type `E` with a defined distance `dist`, the triangle inequality holds: `dist (x x) (z x) ≤ dist (x x) (y x) + dist (y x) (z x)`.
|
PiNat.apply_eq_of_lt_firstDiff
theorem PiNat.apply_eq_of_lt_firstDiff :
∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, n < PiNat.firstDiff x y → x n = y n
This theorem states that for any two functions `x` and `y` from natural numbers to a type `E` indexed by natural numbers, and for any natural number `n`, if `n` is less than the first index where `x` and `y` differ (denoted as `PiNat.firstDiff x y`), then the values of `x` and `y` at index `n` are equal. Essentially, for any index before the first differing index, the two functions `x` and `y` have the same values.
More concisely: For any functions `x` and `y` from natural numbers to type `E`, if `n` is less than the first index where they differ, then `x n = y n`.
|
PiNat.dist_comm
theorem PiNat.dist_comm : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), dist x y = dist y x
This theorem states that the distance function `dist` in the space of dependent functions (indexed by natural numbers, `ℕ`) is commutative. In other words, for any two functions `x` and `y` where each function maps a natural number `n` to a value of type `E n`, the distance from `x` to `y` is the same as the distance from `y` to `x`.
More concisely: For any two dependent functions `x` and `y` : ℕ → E, the commutativity of the distance function `dist` holds: dist (x _) (y _) = dist (y _) (x _).
|
PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder
theorem PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder :
∀ {E : ℕ → Type u_1} {α : Type u_2} [inst : PseudoMetricSpace α] {f : ((n : ℕ) → E n) → α},
(∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔
∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ PiNat.cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n
This theorem is about a function mapping sequences to a pseudo-metric space. It states that the function is 1-Lipschitz if and only if for any two sequences `x` and `y`, and any natural number `n`, if `y` belongs to the cylinder of length `n` around `x` (i.e. `y` coincides with `x` for the first `n` terms), then the distance between the images of `x` and `y` under the function is less than or equal to `(1/2)^n`. The term "1-Lipschitz" here means that the function doesn't increase distances between points, specifically, the distance between `f(x)` and `f(y)` is less than or equal to the distance between `x` and `y`. The theorem does not use the `LipschitzWith` definition because the domain of the function, a sequence space, doesn't have a metric space structure.
More concisely: A function mapping sequences to a pseudo-metric space is 1-Lipschitz if and only if for any sequences x and y and natural number n, if y is a sub-sequence of x of length n, then the distance between their images under the function is less than or equal to (1/2)^n.
|
PiNat.exists_retraction_of_isClosed
theorem PiNat.exists_retraction_of_isClosed :
∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [inst_1 : ∀ (n : ℕ), DiscreteTopology (E n)]
{s : Set ((n : ℕ) → E n)}, IsClosed s → s.Nonempty → ∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ Continuous f
This theorem, named "PiNat.exists_retraction_of_isClosed", states the following:
For any function `E` from natural numbers to some types `u_1`, where each type `u_1` has a topological structure and a discrete topology, and given a closed, nonempty subset `s` of the function space from natural numbers to `E n` (denoted as `(n : ℕ) → E n`), there exists a function `f` that retracts the space onto the subset `s`. This means that `f` is continuous, its range equals to `s`, and it behaves as the identity function when restricted to `s`. In other words, for every element `x` in `s`, `f(x)` equals `x`.
This theorem provides the existence of a retraction in a certain function space, which is an important concept in topology related to the properties of spaces and subsets.
More concisely: Given a closed, nonempty subset `s` of the function space from natural numbers to types `u_1` with discrete topology, there exists a continuous function `f` such that `f(x) = x` for all `x` in `s`.
|
PiNat.firstDiff_comm
theorem PiNat.firstDiff_comm : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), PiNat.firstDiff x y = PiNat.firstDiff y x
The theorem `PiNat.firstDiff_comm` states that for any function `E` from natural numbers to some type, and any two elements `x` and `y` in the product space generated by `E`, the function `PiNat.firstDiff` commutes. In other words, the first index at which `x` and `y` differ is the same as the first index at which `y` and `x` differ. This means the order in which you compare `x` and `y` does not affect the outcome of `PiNat.firstDiff`.
More concisely: For any function from natural numbers to some type and any two elements of its product space, the indices at which they first differ are equal.
|
PiNat.dist_self
theorem PiNat.dist_self : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n), dist x x = 0
This theorem, `PiNat.dist_self`, states that for all functions `x` from natural numbers `ℕ` to some type `Type u_1`, the distance between `x` and itself is `0`. This essentially means that any function from natural numbers to any type is at a 'distance' of zero from itself.
More concisely: For any function `x : ℕ → Type u_1`, the distance from `x` to itself is `0`.
|
PiNat.cylinder_eq_res
theorem PiNat.cylinder_eq_res :
∀ {α : Type u_2} (x : ℕ → α) (n : ℕ), PiNat.cylinder x n = {y | PiNat.res y n = PiNat.res x n}
The theorem `PiNat.cylinder_eq_res` states that for every natural number sequence `x` and a given natural number `n`, the cylinder of `x` at `n` (which is the set of sequences `y` that agree with `x` on the first `n` terms) is equivalent to the set of sequences `y` whose restriction to `n` is the same as the restriction of `x` to `n`. In other words, a sequence `y` belongs to the cylinder of `x` at `n` if and only if the first `n` terms of `y` match the first `n` terms of `x`.
More concisely: The cylinder of a sequence `x` at `n` equals the set of sequences `y` such that the first `n` terms of `y` are equal to the first `n` terms of `x`.
|
PiNat.exists_lipschitz_retraction_of_isClosed
theorem PiNat.exists_lipschitz_retraction_of_isClosed :
∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [inst_1 : ∀ (n : ℕ), DiscreteTopology (E n)]
{s : Set ((n : ℕ) → E n)},
IsClosed s → s.Nonempty → ∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ LipschitzWith 1 f
The theorem `PiNat.exists_lipschitz_retraction_of_isClosed` states that for a given closed nonempty subset `s` of a function space `Π (n : ℕ), E n` (where `E n` is a topological space and `n` ranges over natural numbers), there exists a Lipschitz map `f` with Lipschitz constant `1`, such that the range of `f` is exactly `s`, and `f` acts as the identity function on `s`. In other words, `f` "retracts" the entire space onto the set `s` in a Lipschitz manner, and is unchanged on `s`. This provides a retraction property which is often required in fixed-point theorems and various aspects of mathematical analysis.
More concisely: Given a closed nonempty subset `s` of the function space `Π (n : ℕ), E n`, there exists a Lipschitz map `f` with Lipschitz constant `1` such that `f` acts as the identity on `s` and maps `s` bijectively onto its range.
|
Mathlib.Topology.MetricSpace.PiNat._auxLemma.7
theorem Mathlib.Topology.MetricSpace.PiNat._auxLemma.7 :
∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, (y ∈ PiNat.cylinder x n) = ∀ i < n, y i = x i
The theorem `Mathlib.Topology.MetricSpace.PiNat._auxLemma.7` states that for any set of types `E` indexed by natural numbers, any two sequences `x` and `y` of elements of the types `E` indexed by natural numbers, and any natural number `n`, the condition for `y` to be in the cylinder set of `x` of length `n` is that for every `i` less than `n`, the `i`th element of `y` equals the `i`th element of `x`. In other words, `y` is in the cylinder set of `x` of length `n` if and only if the first `n` elements of `y` and `x` are identical.
More concisely: For any sequence of types indexed by natural numbers E, and any two sequences x and y of elements from E, the sequence y belongs to the cylinder set of length n around x if and only if the first n elements of y are equal to the first n elements of x.
|
PiNat.res_eq_res
theorem PiNat.res_eq_res :
∀ {α : Type u_2} {x y : ℕ → α} {n : ℕ}, PiNat.res x n = PiNat.res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m
The theorem `PiNat.res_eq_res` states that, for any type `α` and for any two functions `x` and `y` from natural numbers to `α`, and for any natural number `n`, the restriction of `x` and `y` to `n` are equal if and only if `x m = y m` for all `m < n`. Here, the restriction of a function to `n` is a list consisting of the first `n` entries of that function. This means that two functions `x` and `y` have the same restrictions up to `n` if and only if they have the same values for all natural numbers less than `n`.
More concisely: For functions `x` and `y` from natural numbers to type `α`, their restrictions to the first `n` natural numbers are equal if and only if `x n = y n` for all `n`.
|
PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff
theorem PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff :
∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [inst_1 : ∀ (n : ℕ), DiscreteTopology (E n)]
{x y : (n : ℕ) → E n} {s : Set ((n : ℕ) → E n)},
IsClosed s →
s.Nonempty →
PiNat.longestPrefix x s < PiNat.firstDiff x y →
x ∉ s → y ∉ s → PiNat.cylinder x (PiNat.longestPrefix x s) = PiNat.cylinder y (PiNat.longestPrefix y s)
The theorem `PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff` states that given a product space, denoted as `Π n, E n`, two sequences `x` and `y` in this space, and a closed, non-empty subset `s` of this space, if `x` and `y` sequences have the same prefix up to a length `n`, and the longest common prefix of sequence `x` with the subset `s` is strictly shorter than `n`, then the longest common prefix of sequence `y` with the subset `s` is the same. Furthermore, the cylinder sets of this length - which are defined as the set of sequences that coincide with `x` and `y` respectively on the first `n` symbols - coincide. The theorem also assumes that neither `x` nor `y` belong to the set `s`.
In simpler terms, if two sequences are identical up to a certain point, and they both have their longest common prefix with a given set shorter than that point, then the longest common prefix of both sequences with the set is the same, and the corresponding 'cylinders' (sets of sequences matching up to that prefix) are equal.
More concisely: Given a product space `Π n, E n`, two sequences `x` and `y` not in a closed, non-empty subset `s`, if `x` and `y` have the same prefix of length `n` and their longest common prefix with `s` is strictly shorter than `n`, then their longest common prefixes with `s` are equal, and the corresponding cylinder sets are equal.
|
PiNat.mem_cylinder_firstDiff
theorem PiNat.mem_cylinder_firstDiff :
∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), x ∈ PiNat.cylinder y (PiNat.firstDiff x y)
The theorem `PiNat.mem_cylinder_firstDiff` states that for any two sequences `x` and `y` in a product space `Π n, E n` (where `E` is a function from the set of natural numbers to some type), the sequence `x` belongs to the cylinder set around `y` of length equal to the first index at which `x` and `y` differ, as indicated by `PiNat.firstDiff x y`. In other words, the sequences `x` and `y` are identical up to the index given by `PiNat.firstDiff x y`, and this index is the length of the cylinder set that `x` belongs to.
More concisely: For any sequences `x` and `y` in a product space `Π n, E n`, `x` belongs to the cylinder set around `y` of length `PiNat.firstDiff x y`.
|
PiNat.firstDiff_def
theorem PiNat.firstDiff_def :
∀ {E : ℕ → Type u_2} (x y : (n : ℕ) → E n), PiNat.firstDiff x y = if h : x ≠ y then Nat.find ⋯ else 0
The theorem `PiNat.firstDiff_def` states that for any sequence of types `E` indexed by natural numbers, and given two functions `x` and `y` from natural numbers to these types, the value of `PiNat.firstDiff x y` is defined as follows: If `x` and `y` are not equal (`x ≠ y`), then `PiNat.firstDiff x y` is the smallest natural number at which `x` and `y` differ, denoted by `Nat.find`. If `x` and `y` are equal (`x = y`), then by convention `PiNat.firstDiff x y` is set to `0`.
More concisely: For any sequences `x` and `y` of types indexed by natural numbers, `PiNat.firstDiff x y` is the smallest index where `x` and `y` differ if they are not equal, and is equal to 0 if they are equal.
|
exists_nat_nat_continuous_surjective_of_completeSpace
theorem exists_nat_nat_continuous_surjective_of_completeSpace :
∀ (α : Type u_2) [inst : MetricSpace α] [inst_1 : CompleteSpace α] [inst_2 : SecondCountableTopology α]
[inst_3 : Nonempty α], ∃ f, Continuous f ∧ Function.Surjective f
This theorem states that for any nonempty complete second countable metric space, denoted as `α`, there exists a function `f` that is both continuous and surjective. In other words, we can map the space of natural to natural numbers, `ℕ → ℕ`, to any point in this metric space `α` using a continuous function `f`, and every point in `α` can be reached by some natural number pair under this function. A similar version of this theorem is also applicable in the context of Polish spaces.
More concisely: For any nonempty complete second countable metric space, there exists a continuous surjection from the natural numbers to the space.
|