Pi.uniformContinuous_precomp'
theorem Pi.uniformContinuous_precomp' :
∀ {ι : Type u_1} {ι' : Type u_2} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (φ : ι' → ι),
UniformContinuous fun f j => f (φ j)
The theorem `Pi.uniformContinuous_precomp'` states that for any two types `ι` and `ι'`, a function `α : ι → Type u` mapping each element of `ι` to a type with a uniform space structure, and a function `φ : ι' → ι`, the function `f` that maps each element `j` of `ι'` to `f (φ j)`, is uniformly continuous. In other words, if `j` is sufficiently close to some other element in `ι'`, then `f (φ j)` is close to `f (φ j')` for any `j` and `j'` in `ι'`, regardless of their specific locations in `ι'`.
More concisely: Given types `ι` and `ι'`, a function `α : ι → Type u` with uniform space structure, and a function `φ : ι' → ι`, the function `f : ι' → α (φ)` is uniformly continuous.
|
uniformContinuous_pi
theorem uniformContinuous_pi :
∀ {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] {β : Type u_4} [inst : UniformSpace β]
{f : β → (i : ι) → α i}, UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i
The theorem `uniformContinuous_pi` states that for any index type `ι` and any family of types `α : ι → Type` equipped with uniform spaces, for any type `β` also equipped with a uniform space, and for any function `f : β → (i : ι) → α i`, the function `f` is uniformly continuous if and only if for each index `i : ι`, the function `fun x => f x i` is uniformly continuous. In other words, a function from `β` to a family of types `α i` is uniformly continuous if and only if its projections to each `α i` are uniformly continuous.
More concisely: A function from a uniform space to a family of types, each equipped with a uniform structure, is uniformly continuous if and only if the projection functions to each type are uniformly continuous.
|
Pi.uniformContinuous_postcomp'
theorem Pi.uniformContinuous_postcomp' :
∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] {β : ι → Type u_4}
[inst : (i : ι) → UniformSpace (β i)] {g : (i : ι) → α i → β i},
(∀ (i : ι), UniformContinuous (g i)) → UniformContinuous fun f i => g i (f i)
The theorem `Pi.uniformContinuous_postcomp'` states that if for every index `ι` in a given set, a function `g` mapping from a uniform space `α` to another uniform space `β` is uniformly continuous, then the function composition of `g` and another function `f`, where `f` takes an index `i` and returns an element in `α` at that index, is also uniformly continuous. In other words, for any index `i`, if `g(i)` is uniformly continuous, then the composite function `(g(i) ∘ f(i))` is also uniformly continuous. This theorem is a statement about the preservation of uniform continuity under function composition in the context of indexed sets of uniform spaces.
More concisely: If, for each index `ι`, a uniformly continuous function `g(ι) : α → β` is composed with a function `f : ℛ → α` that maps indices to elements in `α`, the resulting composite function `g(f(ι)) : ℛ → β` is also uniformly continuous.
|
Pi.uniformity
theorem Pi.uniformity :
∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)],
uniformity ((i : ι) → α i) = ⨅ i, Filter.comap (fun a => (a.1 i, a.2 i)) (uniformity (α i))
This theorem states that for any type `ι` and a function `α` from `ι` to a type `u`, given a uniform space structure `U` for each `α i`, the uniformity of the function space `(i : ι) → α i` is equal to the infimum over `i` of the filter obtained by the comap (preimage under a function) of the function `(a => (a.1 i, a.2 i))` on the uniformity of each `α i`. In simpler terms, it describes how the uniformity of a function space can be constructed from the uniformities of its component spaces.
More concisely: The uniformity of a function space from a type `ι` to a uniform space `u`, given a uniformity structure on each component space, is the infimum of the filters obtained by taking the preimages of the uniformity under the projection functions.
|
Pi.uniformSpace_eq
theorem Pi.uniformSpace_eq :
∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)],
Pi.uniformSpace α = ⨅ i, UniformSpace.comap (Function.eval i) (U i)
The theorem `Pi.uniformSpace_eq` states that, for any index type `ι` and any family `α` of types indexed over `ι` where each type in the family is equipped with a uniform space `U`, the uniform space of the product type (denoted as `Pi.uniformSpace α`) is equal to the infimum of the collection of uniform spaces obtained by applying the `comap` function to the projection functions `(fun a => a i)` and the corresponding uniform space `U i` for each index `i`. Here, `UniformSpace.comap` describes the operation of pulling back a uniform space along a function, and `⨅ i` represents the infimum (or greatest lower bound) over all indices `i`.
More concisely: The uniform space of a product type of uniform spaces indexed over a type, equipped with the projections as functions, is equal to the infimum of the uniform spaces pulled back via these projections.
|
Pi.uniformContinuous_proj
theorem Pi.uniformContinuous_proj :
∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (i : ι), UniformContinuous fun a => a i := by
sorry
This theorem states that for any index set `ι` and any family of types `α` indexed by `ι`, where each type in the family has a uniform space structure, the projection function that assigns to each element in the product space the coordinate corresponding to a fixed index `i` is uniformly continuous. In other words, if `a` is close to `b` in the product space, then the `i`-th coordinates of `a` and `b` are also close, regardless of the location of `a` and `b` in the product space.
More concisely: For any indexed family of uniform spaces `(α\_i : i ∈ ι)` and their product space `Π i, α\_i`, the projection function `π\_i : Π x, α\_i (π i x) ︙ α\_i` is uniformly continuous.
|