LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.UniformSpace.Basic

`uniformity_eq_symm` theorem uniformity_eq_symm : ∀ {α : Type ua} [inst : UniformSpace α], uniformity α = Prod.swap <$> uniformity α := by sorry This theorem states that for any type `α` which has a `UniformSpace` structure, the uniformity of `α` is equal to the uniformity of `α` after swapping the factors of the product. In other words, the uniform distribution on the product space `α × α` is symmetric; the distribution remains the same when the factors are swapped. This is crucial when considering properties such as convergence and continuity in a uniform space, as they should be insensitive to the order of the factors. More concisely: For any type `α` with a `UniformSpace` structure, the uniformity of `α × α` is equal to the swapped product uniformity.
`UniformSpace.le_sInf` theorem UniformSpace.le_sInf : ∀ {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α}, (∀ t' ∈ tt, t ≤ t') → t ≤ sInf tt The theorem `UniformSpace.le_sInf` is a statement about uniform spaces. Given a type `α` and a set `tt` of uniform spaces on `α`, as well as a particular uniform space `t` on `α`, this theorem states that if `t` is less than or equal to every uniform space in set `tt`, then `t` is also less than or equal to the infimum (greatest lower bound) of the set `tt`. In other words, this theorem ensures that `t` respects the order defined by the set `tt` in the context of the infimum operation. More concisely: If `t` is a uniform space on `α` that is less than or equal to every uniform space `u` in a set `tt` of uniform spaces on `α`, then `t` is less than or equal to the infimum of `tt`.
`mem_nhds_left` theorem mem_nhds_left : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) {s : Set (α × α)}, s ∈ uniformity α → {y \| (x, y) ∈ s} ∈ nhds x This theorem states that for any type `α` equipped with a Uniform Space structure, any element `x` of `α`, and any set `s` of pairs of elements from `α` that is in the uniformity of `α`, the set of all elements `y` such that `(x, y)` is in `s` belongs to the neighborhood filter of `x`. In simpler terms, it states that if we have a set of pairs that is 'close' according to the uniformity of the space, then the set of all 'partners' of `x` within that set is a neighborhood of `x`. This theorem is about the relationship between uniform spaces and the concept of neighborhood in topology. More concisely: For any uniform space `(α, Σ)` and `x ∈ α`, if `s ∈ Σ` and `(x, y) ∈ s`, then `y ∈ νx` where `νx` is the neighborhood filter of `x`.
`Mathlib.Topology.UniformSpace.Basic._auxLemma.1` theorem Mathlib.Topology.UniformSpace.Basic._auxLemma.1 : ∀ {α : Type ua} {a b : α}, ((a, b) ∈ idRel) = (a = b) := by sorry This theorem states that for any type `α` and any two elements `a` and `b` of type `α`, the pair `(a, b)` is in the identity relation `idRel` if and only if `a` and `b` are equal. In other words, `idRel` essentially captures the notion of equality for the type `α`. More concisely: For any type `α` and any elements `a` and `b` of type `α`, `(a, b)` is in the identity relation `idRel` if and only if `a = b`.
`symm_le_uniformity` theorem symm_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.map Prod.swap (uniformity α) ≤ uniformity α This theorem states that for any type `α` that has an associated uniform space structure, the forward map of the uniformity of `α` under the product swap operation is less than or equal to the uniformity of `α`. In other words, if we take the uniformity (which is a filter on the product `α × α`) and apply the product swap operation (which swaps the elements of an ordered pair), the resulting mapped filter is still less than or equal to the original uniformity. This theorem is fundamental in the theory of uniform spaces, ensuring a sort of symmetry property for the uniformity filter. More concisely: The forward map of a uniformity on a type under the product swap operation is less than or equal to the original uniformity.
`mem_nhds_uniformity_iff_right` theorem mem_nhds_uniformity_iff_right : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ {p \| p.1 = x → p.2 ∈ s} ∈ uniformity α This theorem states that for any type `α` equipped with a `UniformSpace` structure, any point `x` of type `α`, and any set `s` of type `α`, `s` is a neighborhood of `x` (i.e., `s` belongs to the neighborhood filter at `x`) if and only if the set of pairs `p` such that if the first component of `p` is `x`, then the second component of `p` belongs to `s`, belongs to the uniformity filter of `α`. In simpler terms, it connects the concepts of neighborhood filters and the uniformity filter in a uniform space, specifying how a set qualifies as a neighborhood of a particular point under the conditions of uniform space. More concisely: In a uniform space, a set is a neighborhood of a point if and only if the point-set pair lies in the uniformity relation.
`AddOpposite.uniformContinuous_unop` theorem AddOpposite.uniformContinuous_unop : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous AddOpposite.unop This theorem states that for any type `α` that has a uniform space structure, the unop function from the additive opposite of `α` to `α` is uniformly continuous. In mathematical terms, this means irrespective of where two elements are situated in the additive opposite space, if they are sufficiently close to each other, then their images under the unop function are also close in `α`. Therefore, the unop function preserves the closeness of elements when mapping from the additive opposite space to the original space, which is the characteristic property of uniformly continuous functions. More concisely: The unop function from the additive opposite of a uniform space `α` is uniformly continuous.
`uniformContinuous_inf_dom_right₂` theorem uniformContinuous_inf_dom_right₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}, (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2 The theorem `uniformContinuous_inf_dom_right₂` states that for any types `α`, `β`, and `γ`, and any function `f` from `α × β` to `γ`, given multiple uniform structures on `α`, `β`, and `γ`, if `f` is uniformly continuous under one set of uniform structures, then `f` remains uniformly continuous under the same function definition. In other words, the uniform continuity of a binary function doesn't depend on the specific uniform structures chosen for its domain and codomain. More concisely: If a binary function is uniformly continuous with respect to one choice of uniform structures on its domain and codomain, then it is uniformly continuous with respect to any other compatible choices.
`lebesgue_number_of_compact_open` theorem lebesgue_number_of_compact_open : ∀ {α : Type ua} [inst : UniformSpace α] {K U : Set α}, IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ uniformity α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U The theorem `lebesgue_number_of_compact_open` states the following in mathematics: Given any type `α` that is equipped with a `UniformSpace` structure, and any two sets `K` and `U` of type `α`, if `K` is a compact set and `U` is an open set, and `K` is a subset of `U`, then there exists an open set `V` (referred to as an 'entourage' in the context of uniform spaces) such that `V` is in the uniformity filter of `α` and for every point `x` in `K`, the 'ball' of size `V` centered at `x` is a subset of `U`. In more casual language, this theorem is saying that given any compact set within an open set, there's always an amount of "wiggle room" (the set `V`) such that any point in the compact set can "wiggle" within this room without leaving the open set. The size of the "wiggle room" is the same for all points in the compact set. This is a consequence of the Lebesgue number lemma in the realm of uniform spaces. More concisely: Given a compact set `K` in a uniform space and an open set `U` containing `K`, there exists an open set `V` such that for all `x` in `K`, the open ball `B(x,r)` with radius `r` from `x` is a subset of `U` for some `r` determined by `V`.
`UniformSpace.Core.comp` theorem UniformSpace.Core.comp : ∀ {α : Type u} (self : UniformSpace.Core α), (self.uniformity.lift' fun s => compRel s s) ≤ self.uniformity := by sorry This theorem states that for every type α equipped with a uniform space structure, and for every set `u` in the uniformity of this type, there exists a set `v` in the same uniformity such that the composition of `v` with itself (denoted `v ○ v`) is a subset of `u`. This theorem is a property of uniform spaces and describes a sort of "transitivity" in the uniformity filter. More concisely: For every uniform space (α, Ξ), and for every open set u in Ξ, there exists an open set v in Ξ such that v ○ v ⊆ u.
`UniformContinuous.subtype_mk` theorem UniformContinuous.subtype_mk : ∀ {α : Type ua} {β : Type ub} {p : α → Prop} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (h : ∀ (x : β), p (f x)), UniformContinuous fun x => ⟨f x, ⋯⟩ This theorem states that for every function `f` from type `β` to `α`, if `f` is uniformly continuous and if for every element `x` of type `β`, `p (f x)` holds (i.e., the image of `x` under `f` satisfies a certain property `p`), then the function which maps each `x` of type `β` to a subtype `{ val := f x, property := ⋯ }` of `α` (where each element in the subtype is an element of `α` that satisfies the property `p`) is also uniformly continuous. This means, no matter where the elements of `β` are located, if they are sufficiently close to each other then their images under this new function are also close to each other. More concisely: If `f` is a uniformly continuous function from type `β` to `α` and `p(x)` holds for every `x` in `β`, then the function mapping each `x` to the subtype of elements in `α` satisfying `p(x)` is also uniformly continuous.
`compRel_mono` theorem compRel_mono : ∀ {α : Type ua} {f g h k : Set (α × α)}, f ⊆ h → g ⊆ k → compRel f g ⊆ compRel h k The theorem `compRel_mono` states that for all types `α` and for all relations `f`, `g`, `h`, and `k` on `α`, if `f` is a subset of `h` and `g` is a subset of `k`, then the composition of the relations `f` and `g` is a subset of the composition of the relations `h` and `k`. Here, the composition of two relations is defined as the set of pairs `(a, b)` such that there exists an element `z` where `(a, z)` belongs to the first relation and `(z, b)` belongs to the second relation. More concisely: If relations $f \subseteq h$ and $g \subseteq k$ on type $\alpha$, then $f \circ g \subseteq h \circ k$, where $\circ$ denotes relation composition.
`eventually_uniformity_iterate_comp_subset` theorem eventually_uniformity_iterate_comp_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set (α × α)}, s ∈ uniformity α → ∀ (n : ℕ), ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, (fun x => compRel t x)^[n] t ⊆ s The theorem `eventually_uniformity_iterate_comp_subset` states that, for any type `α` with a `UniformSpace` structure, given a set `s` of pairs of `α` in the uniformity filter of `α`, for every natural number `n`, there exists a subset `t` of a sufficiently small set in the uniformity filter such that the `n-fold` composition of `t` with itself is a subset of `s`. The `n-fold` composition is defined as repeated application of the relation composition `compRel` on `t`. More concisely: For any uniform space `α` and set `s` in its uniformity filter, there exists a subset `t` of a sufficiently small set in the uniformity filter such that the `n-fold` composition of `t` with itself is contained in `s`.
`tendsto_diag_uniformity` theorem tendsto_diag_uniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] (f : β → α) (l : Filter β), Filter.Tendsto (fun x => (f x, f x)) l (uniformity α) This theorem states that for any given type `α` with a uniform space structure, and any function `f` from type `β` to `α` along with a filter `l` on `β`, the function `f` is reflexive with respect to the limit operation on the uniformity of `α`. This is because the mapping from `f` to `(f x, f x)` for all `x` in `β` tends to the uniformity of `α` under the filter `l`. In mathematical terms, this theorem tells us that for all `x` in the domain, the limit of the pairs `(f x, f x)` as `x` approaches any point in the filter `l` exists and is in the uniformity of `α`. More concisely: For any uniform space `(α, εα)`, function `f : β → α`, and filter `l` on `β`, the limit of the constant function `λx. (f x, f x)` exists in the uniformity of `α` with respect to `l`.
`UniformSpace.comap_iInf` theorem UniformSpace.comap_iInf : ∀ {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ι → UniformSpace γ} {f : α → γ}, UniformSpace.comap f (⨅ i, u i) = ⨅ i, UniformSpace.comap f (u i) This theorem states that for any indexing type `ι`, any types `α` and `γ`, any function `f` from `α` to `γ`, and any family `u` of uniform spaces on `γ` indexed by `ι`, the uniform space on `α` obtained by taking the comap of `f` with the infimum (over `ι`) of the uniform spaces `u i` equals the infimum (over `ι`) of the uniform spaces obtained by taking the comap of `f` with each `u i`. In other words, the process of taking the comap of a function with a uniform space commutes with taking the infimum of a family of uniform spaces. More concisely: For any indexing type `ι`, type `α`, type `γ`, function `f` from `α` to `γ`, and family `u` of uniform spaces on `γ` indexed by `ι`, the uniform space on `α` obtained by composing `f` with the infimum of `u` equals the infimum of the uniform spaces obtained by composing `f` with each `u i`.
`nhdsSet_diagonal_le_uniformity` theorem nhdsSet_diagonal_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], nhdsSet (Set.diagonal α) ≤ uniformity α This theorem states that for any type `α` equipped with a `UniformSpace` instance, the filter of neighborhoods of the diagonal set in `α` is less than or equal to the uniformity of `α`. Here, the diagonal set is the set of all pairs `(a, a)`, and the filter of neighborhoods of a set in a topological space is the supremum of the neighborhoods of each point in the set. An entourage is a neighbourhood of the diagonal in the uniformity, so the theorem is essentially asserting that every neighborhood of the diagonal is an entourage. Essentially, this is a way of stating that the uniformity (which describes a kind of "closeness" relation in the space) respects the topological structure of the space. More concisely: For any uniform space `(α, U)`, the filter of neighborhoods of the diagonal set in `α` is contained in `U`.
`uniformContinuous_of_const` theorem uniformContinuous_of_const : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {c : α → β}, (∀ (a b : α), c a = c b) → UniformContinuous c The theorem `uniformContinuous_of_const` states that for any two types `α` and `β` equipped with a UniformSpace structure, any function `c : α → β` that assigns the same value to every element of `α`, i.e., `c a = c b` for all `a` and `b` in `α`, is uniformly continuous. This means that no matter where in the domain `α` two points are, if they are close to each other, their images under `c` are also close. This condition holds trivially for constant functions because the images of all points are the same, and thus always "close". More concisely: A constant function between two uniform spaces is uniformly continuous.
`uniformContinuousOn_iff_restrict` theorem uniformContinuousOn_iff_restrict : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α}, UniformContinuousOn f s ↔ UniformContinuous (s.restrict f) This theorem states that for any types `α` and `β` with uniform space structures, a function `f` from `α` to `β`, and a set `s` of `α`, the function `f` is uniformly continuous on `s` if and only if the restriction of `f` to `s` (i.e., the function obtained by considering `f` only on the elements of `s`) is uniformly continuous. In other words, `f` behaves uniformly on the set `s` precisely when its restriction to `s` is a uniformly continuous function. More concisely: For any uniform spaces `α` and `β`, any uniformly continuous function `f` from `α` to `β`, and any subset `s` of `α`, the restriction of `f` to `s` is uniformly continuous if and only if `f` is uniformly continuous on `s`.
`uniformity_prod_eq_prod` theorem uniformity_prod_eq_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], uniformity (α × β) = Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β) The theorem `uniformity_prod_eq_prod` states that for any two types `α` and `β` which both have `UniformSpace` structures, the uniformity of the product type `(α × β)` is equal to the map of the product of their individual uniformities. In other words, the uniformity over the product space is determined by the individual uniformities over the spaces. The map function takes a pair of pairs and reorders them into a pair of two pairs. This theorem can be seen as a property relating the uniformity structure of a product space to the uniformity structures of its constituent spaces. More concisely: The uniformity of a product type of two uniform spaces is equal to the product of their individual uniformities.
`uniformity_hasBasis_closure` theorem uniformity_hasBasis_closure : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α) closure This theorem states that for any type `α` that has a `UniformSpace` structure, closed entourages form a basis of the uniformity filter. In other words, each entourage in the uniformity filter of `α` can be expressed as the closure of a basis set. Here, an entourage is a set that belongs to the uniformity filter, and the closure of a set `s` is the smallest closed set containing `s`. More concisely: For any uniform space `(α, U)`, the closure of every entourage in `U` is a union of elements in the basis of `U`.
`tendsto_swap_uniformity` theorem tendsto_swap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.Tendsto Prod.swap (uniformity α) (uniformity α) The theorem `tendsto_swap_uniformity` states that for any given type `α` that has a `UniformSpace` structure, the function `Prod.swap` (which swaps the elements of a pair) exhibits a "limit" behavior with respect to the uniformity filter on `α × α`. This means that for every subset of `α × α` that is considered "near" under the uniformity filter, its preimage under `Prod.swap` is also "near" under the uniformity filter. In other words, if a pair of elements is close in the uniformity sense, swapping them does not change their closeness. This suggests a symmetry property in the uniformity structure of the space. More concisely: For any uniform space `α`, the `Prod.swap` function preserves the uniformity relation: for all `x` and `y` in `α × α`, if `x` is uniformly close to `y`, then `Prod.swap x` is uniformly close to `Prod.swap y`.
`comp_le_uniformity3` theorem comp_le_uniformity3 : ∀ {α : Type ua} [inst : UniformSpace α], ((uniformity α).lift' fun s => compRel s (compRel s s)) ≤ uniformity α This theorem, named `comp_le_uniformity3`, states that for any type `α` equipped with a `UniformSpace` structure, the lift' of the uniformity of `α` applied to a function that composes the relation `s` with itself twice (denoted by `compRel s (compRel s s)`) is less than or equal to the uniformity of `α`. The function `compRel` is used to compose relations, and `(uniformity α).lift'` is a method for transforming filters; in this case, it is used to create a new filter by mapping the set of pairs `(x, y)` in the uniformity filter of `α` to a set of all pairs that are related by the composition of relation `s` with itself twice. The theorem essentially asserts that the uniformity derived from the threefold composition of a relation with itself remains within the bounds of the original uniformity. More concisely: For any Type `α` with a uniform structure and relation `s`, the uniformity of `α` is greater than or equal to the uniformity of the composition of `s` with itself twice. (The statement in Lean is stating the converse, that the lifted uniformity of the composition is less than or equal to the original uniformity.)
`uniformContinuous_const` theorem uniformContinuous_const : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {b : β}, UniformContinuous fun x => b The theorem `uniformContinuous_const` asserts that for all types `α` and `β` equipped with uniform space structures, and for any constant `b` in `β`, the function that maps every element of `α` to this fixed constant `b` is uniformly continuous. This means that, no matter how close two points in `α` are (or where they are located in `α`), the corresponding points in `β` (which are both `b`) are always exactly the same. Therefore, the function preserves proximity: if two points are close in `α`, their images are just as close in `β`. More concisely: Given types `α` and `β` with uniform structures and a constant `b` in `β`, the function mapping all of `α` to `b` is a uniformly continuous function.
`MulOpposite.uniformContinuous_unop` theorem MulOpposite.uniformContinuous_unop : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous MulOpposite.unop This theorem states that for any type `α` that has a uniform space structure, the operation `MulOpposite.unop`, which retrieves the original element from its multiplicative opposite, is uniformly continuous. In other words, if two points in the multiplicative opposite space are close to each other, their corresponding points in the original space via `MulOpposite.unop` are also close to each other, regardless of their location in the space. More concisely: For any uniform space `(α, d)` with a multiplicative opposite structure, the map `MulOpposite.unop : α → α` is uniformly continuous with respect to the given metric `d`.
`Filter.HasBasis.uniformContinuous_iff` theorem Filter.HasBasis.uniformContinuous_iff : ∀ {α : Type ua} {β : Type ub} {ι : Sort u_1} [inst : UniformSpace α] {ι' : Sort u_2} [inst_1 : UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)}, (uniformity α).HasBasis p s → ∀ {q : ι' → Prop} {t : ι' → Set (β × β)}, (uniformity β).HasBasis q t → ∀ {f : α → β}, UniformContinuous f ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i The theorem `Filter.HasBasis.uniformContinuous_iff` states that a function `f` from a type `α` to a type `β`, both equipped with uniform space structures, is uniformly continuous if and only if for any index `i` from the index type `ι'` such that the predicate `q` holds on `i`, there exists an index `j` from the index type `ι` satisfying the predicate `p`, and for all pairs `(x, y)` of elements in `α` that belong to the set `s j`, the image pair `(f x, f y)` belongs to the set `t i`. This statement is under the context that the uniformity on `α` has a basis determined by the predicate `p` and the sets `s` indexed by `ι`, and the uniformity on `β` also has a basis determined by the predicate `q` and the sets `t` indexed by `ι'`. The intuition is that `f` is uniformly continuous if it preserves the "closeness" of points in `α` to the "closeness" of points in `β` in a way that corresponds to the basis of their respective uniformities. More concisely: A function between uniform spaces is uniformly continuous if and only if for each basis element in the domain's uniformity, there exists a basis element in the codomain's uniformity such that the corresponding sets satisfy the preservation property.
`nhds_le_uniformity` theorem nhds_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] (x : α), nhds (x, x) ≤ uniformity α This theorem states that for any type `α` equipped with a uniform space structure and any element `x` of `α`, the neighborhood filter of the pair `(x, x)` is less than or equal to the uniformity of `α`. In simpler terms, this is saying that the neighborhoods of the diagonal are also a part of the uniformity structure. In the context of topology, a uniformity provides a precise notion of "closeness" between points, while neighborhoods are sets that contain an open set around a particular point. Therefore, the theorem establishes an important relationship between these two key concepts. More concisely: For any uniform space `(α, υ)`, the neighborhood filter of the diagonal `{(x, x) \| x ∈ α}` is included in the uniformity `υ`.
`UniformSpace.ext` theorem UniformSpace.ext : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, uniformity α = uniformity α → u₁ = u₂ This theorem states that for any given type `α`, and any two uniform spaces `u₁` and `u₂` on `α`, if the uniformity of `α` in both spaces is the same, then the two uniform spaces are indeed identical. In more mathematical terms, this theorem establishes the uniqueness of a uniform space under a given uniformity for a particular type. More concisely: If two uniform spaces on a type `α` have the same uniformity, then they are equal.
`UniformSpace.hasBasis_nhds` theorem UniformSpace.hasBasis_nhds : ∀ {α : Type ua} [inst : UniformSpace α] (x : α), (nhds x).HasBasis (fun s => s ∈ uniformity α ∧ SymmetricRel s) fun s => UniformSpace.ball x s This theorem states that for any type `α` that has a `UniformSpace` structure, and any element `x` of type `α`, the neighborhood filter `nhds x` has a basis that is characterized as follows: The basis elements are those sets `s` that are elements of the uniformity `uniformity α` and for which the relation `SymmetricRel s` holds true. Furthermore, for any such set `s`, the corresponding basis element in the filter `nhds x` is the set `UniformSpace.ball x s`, which can be thought of as the 'ball' around `x` with respect to `s`. In other words, this theorem establishes a connection between the concepts of neighborhood filters, uniformity, symmetric relations, and balls in a uniform space. More concisely: In a uniform space, the neighborhood filter of a point x is exactly the collection of sets in the uniformity that are symmetric around x and generate the uniform topology through their balls as basis elements.
`UniformContinuous.prod_map` theorem UniformContinuous.prod_map : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ] [inst_3 : UniformSpace δ] {f : α → γ} {g : β → δ}, UniformContinuous f → UniformContinuous g → UniformContinuous (Prod.map f g) The theorem `UniformContinuous.prod_map` states that for any four types `α`, `β`, `γ`, `δ` each equipped with a uniform space structure, and any two functions `f : α → γ` and `g : β → δ`, if `f` and `g` are uniformly continuous, then the function `Prod.map f g`, which applies `f` and `g` to the components of a pair respectively, is also uniformly continuous. In mathematical terms, this means that if for any points `x` and `y` in `α` and `β` respectively, `f` and `g` bring `x` and `y` close together as `x` and `y` get close, then the same is true when `f` and `g` are applied to pairs of points in `α × β`. More concisely: If `f : α → γ` and `g : β → δ` are uniformly continuous functions between uniform spaces, then the function `Prod.map f g : α × β → γ × δ` is also uniformly continuous.
`uniformity_prod` theorem uniformity_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], uniformity (α × β) = Filter.comap (fun p => (p.1.1, p.2.1)) (uniformity α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (uniformity β) The theorem `uniformity_prod` states that for any two types `α` and `β` that are equipped with a uniform space structure, the uniformity (which is a filter on the product `α × β`) is equal to the infimum (or greatest lower bound) of the filter obtained by composing the uniformity of `α` with the function that projects onto the first coordinate of both components of a pair, and the filter obtained by composing the uniformity of `β` with the function that projects onto the second coordinate of both components of a pair. Essentially, this theorem describes how the uniformity of a product space is related to the uniformities of the component spaces. More concisely: The uniformity of a product of uniform spaces is the infimum of the uniformity induced by the projection onto the first coordinate and the uniformity induced by the projection onto the second coordinate.
`uniformContinuous_inf_dom_left₂` theorem uniformContinuous_inf_dom_left₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}, (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2 This theorem, named `uniformContinuous_inf_dom_left₂`, states that for any types `α`, `β`, `γ` and a binary function `f` from `α` and `β` to `γ`, if `f` is uniform continuous when considering `α` and `β` as equipped with their first uniform spaces `ua1` and `ub1` and `γ` with its uniform space `uc1`, then `f` remains uniformly continuous when we keep the same uniform spaces. In simpler terms, this theorem ensures the uniform continuity of a binary function remains unchanged under the same uniform spaces. More concisely: If a binary function between three types is uniformly continuous with respect to its first two arguments under given uniform structures, then it remains uniformly continuous with respect to those same uniform structures.
`uniformContinuous_snd` theorem uniformContinuous_snd : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun p => p.2 The theorem `uniformContinuous_snd` states that for any types `α` and `β` both equipped with a uniform space structure, the function that maps any pair `(a, b)` to its second component `b` is uniformly continuous. In other words, as the pair `(a, b)` in `α × β` becomes arbitrarily close to another pair `(a', b')`, the corresponding second components `b` and `b'` become arbitrarily close to each other, regardless of the specific location of `(a, b)` and `(a', b')` within `α × β`. More concisely: Given uniform spaces `(α, δα)` and `(β, δβ)`, the projection function `π₂ : α × β → β` is uniformly continuous.
`Uniform.tendsto_nhds_right` theorem Uniform.tendsto_nhds_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : Filter β} {u : β → α} {a : α}, Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (a, u x)) f (uniformity α) This theorem, `Uniform.tendsto_nhds_right`, states that for any types `α` and `β` with `α` being a uniform space, any filter `f` on `β`, any function `u` from `β` to `α`, and any element `a` of `α`, the function `u` converges to `a` under the filter `f` (denoted as `Filter.Tendsto u f (nhds a)`) if and only if the function that maps each element of `β` to the pair `(a, u x)` tends towards the uniformity on `α` under the filter `f` (denoted as `Filter.Tendsto (fun x => (a, u x)) f (uniformity α)`). In other words, the convergence of `u` to `a` in the topological sense (using neighborhoods of `a`) is equivalent to the convergence in the uniform space sense (using the uniformity filter on `α`). More concisely: For a uniform space `α` and a filter `f` on `β`, a function `u` from `β` to `α` converges to an element `a` in `α` under filter `f` if and only if the function that maps each element `x` in `β` to the pair `(a, u x)` tends towards the uniformity on `α` under filter `f`.
`UniformSpace.hasBasis_symmetric` theorem UniformSpace.hasBasis_symmetric : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun s => s ∈ uniformity α ∧ SymmetricRel s) id The theorem `UniformSpace.hasBasis_symmetric` states that for any type `α` with a `UniformSpace` structure, the filter `uniformity α` has a basis composed of those sets `s` which are both members of `uniformity α` and satisfy the property `SymmetricRel s` (meaning that the set `s` remains the same when the elements of each pair in the set are swapped). In essence, this theorem tells us that we can construct the uniformity of a uniform space using only symmetric neighborhoods. More concisely: The `UniformSpace.hasBasis_symmetric` theorem in Lean 4 asserts that the basis of a uniform space's uniformity consists of symmetric neighborhoods.
`uniformContinuous_sInf_dom₂` theorem uniformContinuous_sInf_dom₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {uas : Set (UniformSpace α)} {ubs : Set (UniformSpace β)} {ua : UniformSpace α} {ub : UniformSpace β} {uc : UniformSpace γ}, ua ∈ uas → ub ∈ ubs → (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2 This theorem, `uniformContinuous_sInf_dom₂`, states that for any three types `α`, `β`, and `γ`, and a binary function `f` from `α` and `β` to `γ`, if we have sets of uniform spaces `uas` and `ubs` on `α` and `β` respectively, along with three uniform spaces `ua`, `ub`, and `uc` on `α`, `β`, and `γ` respectively, then if `ua` belongs to `uas` and `ub` belongs to `ubs` and the function `f` is uniform continuous when viewed as a function from pairs of `α` and `β` to `γ`, it follows that `f` remains uniform continuous when viewed as a function from pairs to `γ`. In simpler terms, the theorem asserts that if a binary function is uniformly continuous in a certain uniform space, then it remains uniformly continuous even if the uniform spaces on its domain types are part of larger sets of uniform spaces. More concisely: If `f` is a uniformly continuous binary function between uniform spaces `(α, uas)` and `(β, ubs)`, then `f` is also uniformly continuous as a function between the product uniform spaces `(α × β, uas ⊓ ubs)` and `(γ, uc)`.
`uniformity_hasBasis_open_symmetric` theorem uniformity_hasBasis_open_symmetric : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V ∧ SymmetricRel V) id The theorem `uniformity_hasBasis_open_symmetric` states that for any type `α` with an associated `UniformSpace` instance, the uniformity of `α` is based on a particular set of conditions. This set contains elements `V` where `V` belongs to the uniformity of `α`, `V` is an open set (in the topological sense), and `V` is symmetric, meaning that the relation `(x, y) ∈ V` is equivalent to `(y, x) ∈ V`. More concisely: For any uniform space `(α, Uniformity)`, the uniformity is generated by the open, symmetric sets.
`symmetric_symmetrizeRel` theorem symmetric_symmetrizeRel : ∀ {α : Type ua} (V : Set (α × α)), SymmetricRel (symmetrizeRel V) This theorem states that for any type `α` and any relation `V` defined as a set of ordered pairs of `α`, the result of the `symmetrizeRel` operation on `V` is a symmetric relation. Here, `symmetrizeRel` operation is used to take a relation and generate the maximal symmetric relation that is a subset of the given relation, while a relation is said to be symmetric if swapping the elements of each pair doesn't change the relation. More concisely: For any type `α` and relation `V` on `α`, the `symmetrizeRel V` relation is symmetric.
`UniformSpace.Core.refl` theorem UniformSpace.Core.refl : ∀ {α : Type u} (self : UniformSpace.Core α), Filter.principal idRel ≤ self.uniformity This theorem states that for any type `α` with a given `UniformSpace.Core` structure, every set in the uniformity filter of that space contains the identity relation, which is also referred to as the diagonal. In other words, the filter generated by the identity relation (which includes all sets containing the diagonal) is a subset of the uniformity filter of the structure. In mathematical terms, if we imagine `α` as a set of points and the uniformity filter as a way of describing 'closeness' between these points, this theorem says that any 'close' pairs of points must include all pairs of identical points. More concisely: For any uniform space `α` with `UniformSpace.Core` structure, the identity relation is included in every set of the uniformity filter.
`union_mem_uniformity_sum` theorem union_mem_uniformity_sum : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {a : Set (α × α)}, a ∈ uniformity α → ∀ {b : Set (β × β)}, b ∈ uniformity β → Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β) The theorem `union_mem_uniformity_sum` states that for any two types `α` and `β` equipped with uniform space structures, and for any set `a` of pairs from `α` that is in the uniformity of `α`, and any set `b` of pairs from `β` that is in the uniformity of `β`, the union of the images of `a` and `b` under the functions `Sum.inl` and `Sum.inr` respectively, is in the uniformity of the disjoint union of `α` and `β`. In other words, if we start with an "entourage" (a certain kind of set of pairs) from each of the two uniform spaces, and if we map each one into the disjoint union space using the appropriate injection, then the union of the results is still an entourage in the disjoint union space. This theorem is an important part of the definition of the uniform structure on the disjoint union of two uniform spaces. More concisely: Given sets `a` in the uniformity of type `α` and `b` in the uniformity of type `β`, the image of their union under `Sum.inl` and `Sum.inr` is in the uniformity of the disjoint union of `α` and `β`.
`Uniform.tendsto_nhds_left` theorem Uniform.tendsto_nhds_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : Filter β} {u : β → α} {a : α}, Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (u x, a)) f (uniformity α) The theorem `Uniform.tendsto_nhds_left` establishes an equivalence between two different ways of representing the limit of a function `u` from a type `β` to a type `α`, where `α` is equipped with a uniform space structure. The first representation is the traditional limit concept, stating that `u` tends to `a` with respect to a filter `f`. The second representation involves the uniformity filter on `α` and states that as elements from the filter `f` are mapped by `u`, the pairs they form with `a` tend to the uniformity of `α`. In other words, the theorem asserts that for every function `u` and every element `a` in a uniform space `α`, `u` tends to `a` with respect to a filter `f` if and only if the pairs formed by mapping elements from `f` through `u` and coupling with `a` tend towards the uniformity filter of `α`. More concisely: For a function `u` from a type `β` to a uniform space `α` and an element `a` in `α`, `u` tends to `a` with respect to a filter `f` if and only if the pairs formed by mapping elements from `f` through `u` and coupling with `a` tend towards the uniformity filter of `α`.
`uniformContinuous_fst` theorem uniformContinuous_fst : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun p => p.1 The theorem `uniformContinuous_fst` states that for any two types `α` and `β` that have UniformSpace instances, the function that takes a pair `p` to its first component `p.1` is uniformly continuous. In other words, if two pairs `(x1, y1)` and `(x2, y2)` are sufficiently close in the UniformSpace of pairs `(α, β)`, then the first components `x1` and `x2` are also sufficiently close in the UniformSpace of `α`. More concisely: If `(α, β)` is a uniform space and `f : α × β → α` is the projection function taking `(x, y)` to `x`, then `f` is uniformly continuous.
`uniformity_prod_eq_comap_prod` theorem uniformity_prod_eq_comap_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], uniformity (α × β) = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β) The theorem `uniformity_prod_eq_comap_prod` states that for any two types `α` and `β` each equipped with a uniformity (i.e. a UniformSpace structure), the uniformity on the product type `α × β` is equal to the filter obtained by applying the `Filter.comap` function to the pair-wise product of the uniformities on `α` and `β`. The function used for the `Filter.comap` takes a product of pairs (from `α × β`) and produces a pair of pairs (for `α` and `β` separately). This theorem, therefore, establishes the connection between the uniform structure on a product type and the uniform structures on the constituent types. More concisely: The uniformity on the product type of two uniform spaces is equal to the composite of their pair-wise product and the `Filter.comap` function.
`subset_comp_self` theorem subset_comp_self : ∀ {α : Type ua} {s : Set (α × α)}, idRel ⊆ s → s ⊆ compRel s s This theorem states that for any type `α` and for any relation `s` which is a set of pairs of `α`, if the identity relation is a subset of `s`, then `s` is a subset of the composition of `s` with itself. In other words, if every pair of identical elements from `α` is in `s`, then for any pair in `s`, there exists an element such that the pair can be split into two pairs which are also in `s`. More concisely: If a relation `s` on type `α` contains the identity relation, then `s` is reflexive and transitive, i.e., `s` is a quadratic closure of itself.
`nhds_eq_comap_uniformity` theorem nhds_eq_comap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = Filter.comap (Prod.mk x) (uniformity α) The theorem `nhds_eq_comap_uniformity` states that for any type `α` endowed with a `UniformSpace` structure, and for any element `x` of `α`, the neighborhood filter at `x` is equal to the comap of the function `Prod.mk x` and the uniformity of `α`. In simpler terms, this means that the set of all neighborhoods (sets containing an open set around `x`) is equivalent to taking the uniformity (a specific filter on the product of `α` with itself) and mapping it back along the function that sends an element to the pair consisting of `x` and that element. This theorem establishes an important correspondence between the concept of a neighborhood in topology and the concept of a uniformity in the context of uniform spaces. More concisely: The neighborhood filter of a point in a uniform space is equal to the composition of the point's evaluation function with the uniformity of the space.
`comap_swap_uniformity` theorem comap_swap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.comap Prod.swap (uniformity α) = uniformity α This theorem states that for any type `α` that has an instance of the `UniformSpace` structure, the filter obtained by applying the `Prod.swap` function through the `Filter.comap` function on the uniformity of `α` is equal to the uniformity of `α`. In simpler terms, swapping the pairs in the uniformity of a uniform space does not change the uniformity. This property is important in the context of uniform spaces, where the concept of "uniformity" is used to generalize the notions of a metric space and topological space, and this property ensures that the uniformity is symmetric. More concisely: For any uniform space `(α, U)`, the filters `U` and `( Прод.swap ∘ Filter.comap U) (pair ∘ pair)` are equal.
`comp_le_uniformity` theorem comp_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], ((uniformity α).lift' fun s => compRel s s) ≤ uniformity α This theorem states that for every type `α` equipped with a UniformSpace structure, the filter obtained by lifting the uniformity of `α` using the function that computes the composition of a relation with itself, is less than or equal to the uniformity of `α`. In other words, within any uniform space, the composition operation applied to any set taken from the uniformity and then lifted onto the uniformity (a form of push-forward), will always yield a set that is still within the bounds of the original uniformity. More concisely: For any uniform space (α, υ), the self-composition lift of its uniformity is a sub-uniformity.
`Filter.HasBasis.mem_uniformity_iff` theorem Filter.HasBasis.mem_uniformity_iff : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {p : β → Prop} {s : β → Set (α × α)}, (uniformity α).HasBasis p s → ∀ {t : Set (α × α)}, t ∈ uniformity α ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t This theorem states that for any types `α` and `β` (with `α` having a `UniformSpace` instance), and any functions `p : β → Prop` and `s : β → Set (α × α)`, if the `uniformity` filter on `α` has a basis defined by these functions (`p` and `s`), then for any set `t` of pairs of `α`, `t` is in the `uniformity` filter on `α` if and only if there exists an `i` in `β` such that `p i` holds and for all elements `a` and `b` of `α`, if the pair `(a, b)` is in the set `s i`, then the pair `(a, b)` is also in `t`. In simpler terms, this theorem provides a condition for a set of pairs of elements of a uniform space to be in the uniformity filter of the space, in terms of the basis of the filter. More concisely: Given a uniform space `α` with `UniformSpace` instance, a property `p : β → Prop`, and a relation `s : β → Set (α × α)` defining a basis for its uniformity filter, a set `t` of pairs of `α` is in the uniformity filter if and only if there exists an `i` in `β` such that `p i` holds and for all `a, b` in `α`, if `(a, b)` is in `s i`, then it is also in `t`.
`uniformContinuous_id` theorem uniformContinuous_id : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous id This theorem states that the identity function is uniformly continuous for any uniform space. In other words, for any type `α` that is a uniform space, the function `id`, which maps each element of `α` to itself, is uniformly continuous. In mathematical terms, this means that as `(x, y)` tends to the diagonal in the space `α`, `(id x, id y)` also tends to the diagonal, meaning that the identity function preserves closeness no matter where `x` and `y` are in `α`. More concisely: The identity function is uniformly continuous on any uniform space.
`nhds_eq_uniformity` theorem nhds_eq_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = (uniformity α).lift' (UniformSpace.ball x) This theorem states that for any type `α` equipped with a uniform space structure and any element `x` of `α`, the neighborhood filter at `x` is equal to the lift via the uniformity filter of `α` of the ball centered at `x`. In other words, the set of all neighborhoods of `x` is obtained by transforming the uniformity filter on `α` using the function that maps each set to the set of all points in `α` that are close to `x` according to the given set. More concisely: For any uniform space `(α, υ)` and `x ∈ α`, the neighborhood filter of `x` is equal to the lift of the ball `B(x, r)` centered at `x` through the uniformity filter `υ`.
`symmetrize_mem_uniformity` theorem symmetrize_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {V : Set (α × α)}, V ∈ uniformity α → symmetrizeRel V ∈ uniformity α := by sorry The theorem `symmetrize_mem_uniformity` states that for any type `α` that has an associated Uniform Space, and for any set `V` of pairs from `α`, if `V` is in the uniformity of `α`, then the symmetrized relation of `V` is also in the uniformity of `α`. Here, symmetrizing a relation means creating a new relation that contains both `(a, b)` and `(b, a)` if and only if the original relation contains `(a, b)`. In other words, the symmetrized relation is the maximal symmetric relation contained in the original relation. More concisely: If `V` is a set of pairs from a uniform space `α`, then the symmetrized relation of `V` is also in the uniformity of `α`.
`uniformContinuous_comap` theorem uniformContinuous_comap : ∀ {α : Type ua} {β : Type ub} {f : α → β} [u : UniformSpace β], UniformContinuous f The theorem `uniformContinuous_comap` states that for any two types `α` and `β`, and for any function `f` mapping from `α` to `β`, if `β` is equipped with a uniform space structure, then the function `f` is uniformly continuous. In the context of mathematics, uniformly continuous means that the closeness of the output values `f(x)` and `f(y)` depends only on the closeness of the input values `x` and `y`, and it does not matter where `x` and `y` are located within the space `α`. More concisely: If `α` is a type and `β` is a uniform space, and `f : α → β` is a function, then `f` is uniformly continuous.
`uniformity_hasBasis_open` theorem uniformity_hasBasis_open : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V) id := by sorry This theorem states that for any type `α` that has a `UniformSpace` instance, the open elements of the uniformity on `α` form a basis of the uniformity. In other words, any element in the uniformity `𝓤 α` can be represented as a "neighborhood" of smaller open sets, where openness is defined with respect to the ambient topological space on `α`. This is a fundamental property of uniform spaces and is crucial for their analysis and manipulation. More concisely: For any uniform space `(α, 𝓤)`, the open sets in `𝓤` form a basis for the uniformity `𝓤`.
`UniformSpace.toTopologicalSpace_iInf` theorem UniformSpace.toTopologicalSpace_iInf : ∀ {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α}, UniformSpace.toTopologicalSpace = ⨅ i, UniformSpace.toTopologicalSpace This theorem states that for any type `α`, any sort `ι`, and any function `u` mapping `ι` to a uniform space over `α`, the topological space derived from the uniform space is equal to the infimum of topological spaces derived from the uniform spaces as per the function `u`. In other words, if you have a collection of uniform spaces indexed by `ι`, the topological space derived from the uniform space is the infimum of the topological spaces derived from each individual uniform space in the collection. More concisely: The topological space derived from a uniform space over a type `α`, indexed by sort `ι`, is equal to the infimum of the topologies derived from each uniform space in the collection.
`UniformSpace.ball_mem_nhds` theorem UniformSpace.ball_mem_nhds : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) ⦃V : Set (α × α)⦄, V ∈ uniformity α → UniformSpace.ball x V ∈ nhds x This theorem states that for any uniform space `α` and any element `x` in `α`, if a set `V` of pairs of elements of `α` belongs to the uniformity of `α`, then the ball centered at `x` with respect to the set `V` belongs to the neighborhood of `x`. In other words, if `V` is a set of pairs describing a certain closeness relationship in the uniform space, then the set of all elements close to `x` according to this relationship is a neighborhood of `x`. This connects the concept of balls in a uniform space, which generalizes the concept of balls in a metric space, to the topological concept of neighborhood. This is a key property that shows the compatibility between the uniform structure and the induced topology in a uniform space. More concisely: For any uniform space `α` and `x` in `α`, if `V` is a set of pairs in the uniformity of `α` then the ball `B(x, V)` is a neighborhood of `x`.
`nhds_basis_uniformity'` theorem nhds_basis_uniformity' : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)}, (uniformity α).HasBasis p s → ∀ {x : α}, (nhds x).HasBasis p fun i => UniformSpace.ball x (s i) The theorem `nhds_basis_uniformity'` states that for any type `α` equipped with a `UniformSpace` structure, and for any index type `ι`, given a filter basis `s` indexed by `ι` on the uniformity of `α`, which satisfies some property `p`, then for each point `x` in `α`, the neighborhood filter at `x` has a filter basis consisting of balls centered at `x` with respect to each set in the given filter basis `s`. In other words, we can generate the neighborhood filter at a point by taking 'balls' around that point, where these balls are defined in terms of sets from the uniformity filter basis of the space. The index set `ι` and property `p` are carried over from the uniformity filter basis to the neighborhood filter basis. More concisely: Given a uniform space (α, U) and a filter basis s on U satisfying property p, for each x in α, the neighborhood filter at x is generated by balls centered at x with respect to sets in s.
`uniformContinuous_comap'` theorem uniformContinuous_comap' : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} {f : γ → β} {g : α → γ} [v : UniformSpace β] [u : UniformSpace α], UniformContinuous (f ∘ g) → UniformContinuous g The theorem `uniformContinuous_comap'` states that for any three types `α`, `β`, and `γ`, and for any two functions `f : γ → β` and `g : α → γ`, where `α` and `β` are equipped with uniform structures, if the composition of `f` and `g` (denoted as `f ∘ g`) is uniformly continuous, then the function `g` is also uniformly continuous. In other words, if for any pair of points `x` and `y` in `α` which are sufficiently close together, `f(g(x))` and `f(g(y))` are also close together in `β`, then `g(x)` and `g(y)` are also close together. This is a property related to the preservation of the uniform continuity under function composition. More concisely: If `f : γ → β` is uniformly continuous and `g : α → γ` is such that `f ∘ g` is uniformly continuous, then `g` is uniformly continuous.
`Filter.Tendsto.uniformity_symm` theorem Filter.Tendsto.uniformity_symm : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {l : Filter β} {f : β → α × α}, Filter.Tendsto f l (uniformity α) → Filter.Tendsto (fun x => ((f x).2, (f x).1)) l (uniformity α) The theorem `Filter.Tendsto.uniformity_symm` states that for any type `α` with a uniform space structure, type `β`, a filter `l` on `β`, and a function `f` mapping `β` to `α × α`, if `f` tends to the uniformity of `α` under the filter `l`, then the function that swaps the components of `f` also tends to the uniformity of `α` under the same filter. Essentially, it asserts the symmetry of the uniform limit of a function with respect to the components of the function's range. More concisely: If a function from a filter on a uniform space to a product space tends to the uniformity of the product space, then the component-wise reversed function also tends to the uniformity.
`UniformSpace.comap_comap` theorem UniformSpace.comap_comap : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {uγ : UniformSpace γ} {f : α → β} {g : β → γ}, UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ) The theorem `UniformSpace.comap_comap` states that for any types `α`, `β`, and `γ`, and any uniform space `uγ` on `γ`, and any functions `f : α → β` and `g : β → γ`, the composition of the comap operation is commutative, i.e., taking the inverse image of the uniformity `uγ` under the composed function `(g ∘ f)` is the same as first taking the inverse image under `g` and then under `f`. In other words, it asserts that the operation of taking "comap" (the inverse image function) over uniform spaces respects composition of functions. The analogy in mathematical terms is that the inverse image operation on uniform spaces is functorial: $(g \circ f)^{-1}(u_\gamma) = f^{-1}(g^{-1}(u_\gamma))$. More concisely: For any functions `f : α → β` and `g : β → γ`, and uniform spaces `uγ` on `γ`, the inverse image of `uγ` under the composition `g ∘ f` is equal to the composition of the inverse images `f^(-1)(g^(-1)(uγ))`.
`idRel_subset` theorem idRel_subset : ∀ {α : Type ua} {s : Set (α × α)}, idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s The theorem `idRel_subset` states that for all types `α` and for all sets `s` of pairs of elements of type `α`, the identity relation is a subset of `s` if and only if for every element `a` of type `α`, the pair `(a, a)` belongs to `s`. In mathematical terms, we can say that the graph of the identity function is a subset of a set `s` if and only if every element in `α` paired with itself is an element of `s`. More concisely: The identity relation on a type `α` is contained in a binary relation `s` if and only if the diagonal elements `(a, a)` of `α` belong to `s`.
`Filter.Tendsto.uniformity_trans` theorem Filter.Tendsto.uniformity_trans : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {l : Filter β} {f₁ f₂ f₃ : β → α}, Filter.Tendsto (fun x => (f₁ x, f₂ x)) l (uniformity α) → Filter.Tendsto (fun x => (f₂ x, f₃ x)) l (uniformity α) → Filter.Tendsto (fun x => (f₁ x, f₃ x)) l (uniformity α) This theorem states that if you have a uniform space `α` and a filter `l` on some type `β`, and if you have three functions `f₁`, `f₂`, and `f₃` from `β` to `α` such that the function from `β` to the product of `α` by `α` that sends `x` to `(f₁ x, f₂ x)` tends to the uniformity of `α` along `l`, and the function sending `x` to `(f₂ x, f₃ x)` also tends to the uniformity of `α` along `l`, then the function sending `x` to `(f₁ x, f₃ x)` will also tend to the uniformity of `α` along `l`. This is the transitivity property for the relation defined by the limit of the function `(f, g) ↦ (f x, g x)` towards the uniformity filter of `α`. More concisely: If two functions from a filter on one type to a uniform space tend to the uniformity of that space along the filter, then their pointwise combination also tends to the uniformity of the space along the filter.
`UniformContinuous.comp` theorem UniformContinuous.comp : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ] {g : β → γ} {f : α → β}, UniformContinuous g → UniformContinuous f → UniformContinuous (g ∘ f) The theorem `UniformContinuous.comp` states that for any three types `α`, `β`, and `γ`, each equipped with a uniform space structure (`UniformSpace α`, `UniformSpace β`, `UniformSpace γ` respectively), if a function `g` from `β` to `γ` is uniformly continuous, and a function `f` from `α` to `β` is uniformly continuous, then the composition of `g` and `f` (denoted by `g ∘ f`) is also uniformly continuous. In other words, the property of uniform continuity is preserved under function composition. More concisely: If functions `f : α → β` and `g : β → γ` are uniformly continuous, then their composition `g ∘ f : α → γ` is also uniformly continuous.
`iSup_nhds_le_uniformity` theorem iSup_nhds_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], ⨆ x, nhds (x, x) ≤ uniformity α This theorem states that, in any uniform space `α`, the supremum (join) of the neighbourhood filters of all points along the diagonal (`x, x`) is less than or equal to the uniformity of `α`. In other words, for each point in the space, the set of all neighbourhoods of that point forms a filter. This filter is less than or equal to the filter that represents the uniformity of the space as a whole. The theorem essentially asserts that the local behaviours at individual points (as captured by neighbourhood filters) are bounded by the global behaviour of the space (as captured by the uniformity). More concisely: For any uniform space `α`, the join of the neighborhood filters of all points `x` in `α` is contained in the uniformity of `α`.
`UniformSpace.ofCoreEq_toCore` theorem UniformSpace.ofCoreEq_toCore : ∀ {α : Type ua} (u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace), UniformSpace.ofCoreEq u.toCore t h = u The theorem `UniformSpace.ofCoreEq_toCore` states that for any type `α`, given a UniformSpace `u` and a TopologicalSpace `t` such that `t` equals the TopologicalSpace generated by the core of `u`, the UniformSpace constructed from the core of `u` and `t` (with the equality condition) is exactly `u`. In other words, this theorem assures that the process of transitioning from a UniformSpace to its core and back to a UniformSpace while retaining the same TopologicalSpace structure, does not change the original UniformSpace. More concisely: For any UniformSpace `u` and TopologicalSpace `t` such that `t` is the topology generated by `u`'s core, the UniformSpace constructed from `u`'s core and `t` is equal to `u`.
`iInf_uniformity` theorem iInf_uniformity : ∀ {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α}, uniformity α = ⨅ i, uniformity α This theorem states that for all types `α` and sorts `ι`, and for a function `u` from `ι` to `UniformSpace α`, the uniformity of the type `α` is equal to the infimum (`⨅`, or greatest lower bound) of the uniformities of the type `α` over all `i` in `ι`. In other words, it means that the uniformity on a certain type `α` in a uniform space context is the greatest lower bound of all the uniformities on `α` given by the function `u` over the index set `ι`. More concisely: The uniformity of a type `α` in a uniform space is the greatest lower bound of the uniformities of `α` under all functions from the index set to `UniformSpace α`.
`UniformSpace.Core.symm` theorem UniformSpace.Core.symm : ∀ {α : Type u} (self : UniformSpace.Core α), Filter.Tendsto Prod.swap self.uniformity self.uniformity This theorem states that for any uniform space, denoted by `α`, and any `s` which is an element of the uniformity of `α`, the preimage of `s` under the function `Prod.swap` (which swaps the elements of ordered pairs) is also an element of the uniformity of `α`. In other words, the uniformity filter of a uniform space is invariant under the swapping of coordinates. This is a formal way of expressing the symmetry property of a uniform space in Lean 4. More concisely: For any uniform space `α` and element `s` of its uniformity, `Prod.swap s` is also an element of the uniformity of `α`.
`ball_mono` theorem ball_mono : ∀ {β : Type ub} {V W : Set (β × β)}, V ⊆ W → ∀ (x : β), UniformSpace.ball x V ⊆ UniformSpace.ball x W This theorem, named `ball_mono`, states that for any type `β` and for any two sets `V` and `W` of pairs of elements of type `β`, if `V` is a subset of `W`, then for any element `x` of type `β`, the ball around `x` with respect to `V` (denoted as `UniformSpace.ball x V`) is a subset of the ball around `x` with respect to `W` (denoted as `UniformSpace.ball x W`). In other words, if a set of pairs `V` is contained within another set of pairs `W`, then the ball centered at any point `x` for `V` will be contained within the ball centered at the same point for `W`. This theorem establishes a key monotonicity property of balls in a uniform space. More concisely: For any type `β` and sets `V` and `W` of pairs of elements of type `β` with `V` being a subset of `W`, the ball around any element `x` of type `β` with respect to `V` (`UniformSpace.ball x V`) is included in the ball around `x` with respect to `W` (`UniformSpace.ball x W`).
`uniformContinuousOn_univ` theorem uniformContinuousOn_univ : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}, UniformContinuousOn f Set.univ ↔ UniformContinuous f The theorem `uniformContinuousOn_univ` states that for any two types `α` and `β` equipped with uniform spaces, and any function `f` from `α` to `β`, the function `f` is uniformly continuous on the universal set of `α` (i.e., the set containing all elements of `α`) if and only if `f` is uniformly continuous. In other words, a function is uniformly continuous in general if it is uniformly continuous when considering all possible inputs. More concisely: A function between uniform spaces is uniformly continuous on the universal set if and only if it is uniformly continuous.
`UniformContinuous.continuous` theorem UniformContinuous.continuous : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}, UniformContinuous f → Continuous f The theorem `UniformContinuous.continuous` states that for all function `f` from a type `α` to a type `β`, where both `α` and `β` have an associated uniform space structure, if `f` is uniformly continuous, then `f` is also continuous. In other words, if for any pair of elements `x` and `y` from `α` that are sufficiently close, their images under `f`, `f x` and `f y`, are also close, then for every point `x` in `α`, the function `f` is continuous at `x`. Here, continuity of `f` means that the preimage of any open set in `β` is open in `α`. More concisely: If a function between uniform spaces is uniformly continuous, then it is continuous.
`uniformContinuous_subtype_val` theorem uniformContinuous_subtype_val : ∀ {α : Type ua} {p : α → Prop} [inst : UniformSpace α], UniformContinuous Subtype.val The theorem `uniformContinuous_subtype_val` states that for any type `α` equipped with a uniform space structure and any predicate `p` on `α`, the function `Subtype.val` is uniformly continuous. In other words, when the inputs of `Subtype.val` (which are elements of a subtype defined by `p`) are sufficiently close to each other, their images (which are elements of the base type `α`) are also close, regardless of where these inputs are located in the subtype. More concisely: For any uniform space `(α, d)` and subtype `s : α → Prop` with predicate `p := ⦃x : α⦄. s x`, the function `Subtype.val : s → α` is uniformly continuous.
`UniformSpace.hasBasis_ofFun` theorem UniformSpace.hasBasis_ofFun : ∀ {α : Type u} {β : Type v} [inst : LinearOrderedAddCommMonoid β], (∃ x, 0 < x) → ∀ (d : α → α → β) (refl : ∀ (x : α), d x x = 0) (symm : ∀ (x y : α), d x y = d y x) (triangle : ∀ (x y z : α), d x z ≤ d x y + d y z) (half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε), (uniformity α).HasBasis (fun x => 0 < x) fun ε => {x \| d x.1 x.2 < ε} This theorem states that for any types `α` and `β`, where `β` is a linearly ordered additive commutative monoid and there exists a positive element in `β`, along with a function `d` mapping two elements of `α` to `β` such that `d` is reflexive, symmetric and satisfies the triangle inequality, and for any `ε > 0`, there exists `δ > 0` such that for all `x, y < δ`, `x + y < ε`. Under these conditions, the uniformity (which is a filter on `α × α` inferred from an ambient uniform space structure on `α`) has a basis such that for all `ε > 0`, the set of pairs `(x.1, x.2)` for which `d x.1 x.2 < ε` belongs to the basis. In other words, the uniformity structure on `α` has a basis which is determined by the distances between elements being less than a certain threshold. More concisely: Given a type `α` with a linearly ordered additive commutative monoid `β` having a positive element, and a function `d` from `α × α` to `β` that is reflexive, symmetric, and satisfies the triangle inequality, there exists a basis for the uniformity on `α` determined by `d` such that for every `ε > 0`, the set of pairs `(x, y)` with `d x y < ε` belongs to the basis.
`lebesgue_number_lemma` theorem lebesgue_number_lemma : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι : Sort u_2} {U : ι → Set α}, IsCompact K → (∀ (i : ι), IsOpen (U i)) → K ⊆ ⋃ i, U i → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ i, UniformSpace.ball x V ⊆ U i The theorem `lebesgue_number_lemma` states that given a compact set `K` in a uniform space `α` and an open cover `U : ι → Set α` of `K` (where each `U i` for `i : ι` is open), there exists an entourage `V` in the uniformity of `α` such that for each element `x` in `K`, there exists an indexing element `i` such that the `V`-neighborhood of `x` (the set of points within `V` distance from `x`) is contained within `U i`. This theorem guarantees the existence of a "Lebesgue number", a certain kind of diameter that provides a uniform measure of how finely `K` can be covered by the open cover `U`. More concisely: Given a compact set in a uniform space and an open cover, there exists an entourage with the property that every point in the set lies in some set of the cover and is contained in that set's corresponding entourage neighborhood.
`comp_symm_mem_uniformity_sets` theorem comp_symm_mem_uniformity_sets : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set (α × α)}, s ∈ uniformity α → ∃ t ∈ uniformity α, SymmetricRel t ∧ compRel t t ⊆ s This theorem states that for any type `α` with a uniform space structure, and for any set `s` of pairs of `α`, if `s` belongs to the uniformity of `α`, then there exists a set `t` within the uniformity of `α`, such that `t` is a symmetric relation and the composition of `t` with itself is a subset of `s`. In other words, any given set in the uniformity of the space can be covered by the composition of a symmetric set from the same uniformity with itself. More concisely: For any uniform space `(α, μ)` and any symmetric relation `t ∈ μ`, if `s ∈ μ` and `s ⊆ t ∘ t`, then there exists a symmetric relation `r ∈ μ` such that `r ∘ r ⊆ s`.
`nhds_basis_uniformity` theorem nhds_basis_uniformity : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)}, (uniformity α).HasBasis p s → ∀ {x : α}, (nhds x).HasBasis p fun i => {y \| (y, x) ∈ s i} The theorem `nhds_basis_uniformity` states that for any type `α` equipped with a `UniformSpace` structure and an index type `ι`, given a filter basis `{p : ι → Prop, s : ι → Set (α × α)}` for the uniformity on `α`, for all `x` in `α`, there exists a filter basis for the neighborhood filter at `x`. This filter basis is indexed by the same index type `ι` and its sets are formed by all `y` in `α` such that `(y, x)` is in the set `s i` for some `i` satisfying `p i`. In simpler terms, it expresses a relationship between the uniformity filter of a uniform space and the neighborhood filters of its points. More concisely: For any uniform space `(α, μ)` and filter basis `{p : ι → Prop, s : ι → α × α}` for `μ`, each point `x` in `α` has a filter basis of neighborhoods given by `{y : α \| ∃ i, p i ∧ (y, x) ∈ s i}`.
`lebesgue_number_lemma_sUnion` theorem lebesgue_number_lemma_sUnion : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {S : Set (Set α)}, IsCompact K → (∀ s ∈ S, IsOpen s) → K ⊆ S.sUnion → ∃ V ∈ uniformity α, ∀ x ∈ K, ∃ s ∈ S, UniformSpace.ball x V ⊆ s This theorem is a version of the Lebesgue's number lemma in the context of uniform spaces. Given a compact set `K` in a uniform space `α` and an open cover `S` of `K`, there exists an entourage (a set of `α × α` in the uniformity filter of `α`) denoted by `V` such that for every point `x` in `K`, there is a set `s` in the open cover `S` which contains the `V`-neighborhood of `x`. In other words, the `V`-neighborhood of each point in the compact set can be covered by some set in the open cover. This theorem is a key result in topological space theory underlying the proof of several important theorems including the Heine-Borel theorem and Tychonoff's theorem. More concisely: Given a compact set in a uniform space and an open cover, there exists an entourage such that each point in the set is contained in the cover of some point in its neighbourhood using the entourage.
`uniformContinuous_iff` theorem uniformContinuous_iff : ∀ {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β}, UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ The theorem `uniformContinuous_iff` states that for any types `α` and `β` equipped with uniform spaces `uα` and `uβ`, and a function `f : α → β`, the function `f` is uniformly continuous if and only if the uniform space `uα` is less than or equal to the uniform space `uβ` under the inverse image map `comap f`. In other words, a function is uniformly continuous if it does not increase the uniformity, i.e., if every entourage (considered as a measure of 'closeness') in `α` is mapped by `f` to an entourage in `β`. More concisely: A function between uniform spaces is uniformly continuous if and only if the inverse image of every entourage in the domain is an entourage in the codomain.
`UniformContinuous.prod_mk` theorem UniformContinuous.prod_mk : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ] {f₁ : α → β} {f₂ : α → γ}, UniformContinuous f₁ → UniformContinuous f₂ → UniformContinuous fun a => (f₁ a, f₂ a) The theorem `UniformContinuous.prod_mk` states that for any types `α`, `β`, and `γ` equipped with uniform space structures, if we have two functions `f₁ : α → β` and `f₂: α → γ` that are both uniformly continuous, then the function that takes an element from `α` and maps it to a pair in `β × γ` where the first element of the pair is the image of the element under `f₁` and the second element of the pair is the image of the same element under `f₂` is also uniformly continuous. In other words, the uniform continuity of individual functions implies the uniform continuity of the function that produces pairs of their outputs. More concisely: If `f₁ : α → β` and `f₂ : α → γ` are uniformly continuous functions between uniform spaces `α`, `β`, and `γ`, then the function `x mapsto (f₁ x, f₂ x)` from `α` to `β × γ` is also uniformly continuous.
`Filter.HasBasis.uniformContinuousOn_iff` theorem Filter.HasBasis.uniformContinuousOn_iff : ∀ {α : Type ua} {β : Type ub} {ι : Sort u_1} [inst : UniformSpace α] {ι' : Sort u_2} [inst_1 : UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)}, (uniformity α).HasBasis p s → ∀ {q : ι' → Prop} {t : ι' → Set (β × β)}, (uniformity β).HasBasis q t → ∀ {f : α → β} {S : Set α}, UniformContinuousOn f S ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i The theorem `Filter.HasBasis.uniformContinuousOn_iff` states that for any types `α` and `β`, any sorts `ι` and `ι'`, given two uniform spaces over `α` and `β`, if the uniformity of `α` has a basis characterized by the property `p` and the set function `s`, and the uniformity of `β` has a basis characterized by the property `q` and the set function `t`, then for any function `f` from `α` to `β` and any set `S` of `α`, the function `f` is uniformly continuous on `S` if and only if for every element `i` of `ι'` such that `q i` holds, there exists an element `j` of `ι` such that `p j` holds and for all `x` and `y` in `S`, if `(x, y)` belongs to `s j` then `(f x, f y)` belongs to `t i`. In simpler terms, it says that a function is uniformly continuous if for a given closeness in the output (β), no matter where we are in the set `S`, we can find a closeness in the input (α) such that if any two points in the set `S` are that close in the input, their images under the function are close in the output. Closeness is defined using the uniformity filters of the respective spaces. More concisely: A function between uniform spaces is uniformly continuous on a set if and only if for every basis element of the target space's uniformity, there exists a basis element of the domain space's uniformity such that their corresponding sets imply the continuity of the function between the elements in the set.
`refl_mem_uniformity` theorem refl_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set (α × α)}, s ∈ uniformity α → (x, x) ∈ s This theorem states that for any type `α` endowed with a `UniformSpace` structure, any point `x` in `α`, and any set `s` of pairs of elements of `α` that is in the uniformity of `α`, the pair `(x, x)` belongs to `s`. In more mathematical terms, it says that if `s` is a set in the uniformity (i.e., a set of "sufficiently close" pairs of points) in a uniform space, then every point of the space is "sufficiently close" to itself according to `s`. This is a formalization of one of the basic properties of uniform spaces: reflexivity of the underlying relation. More concisely: In any uniform space, every point is reflexive with respect to its uniformity, i.e., for any point `x` and any set `s` in the uniformity of `α`, the pair `(x, x)` belongs to `s`.
`mem_ball_comp` theorem mem_ball_comp : ∀ {β : Type ub} {V W : Set (β × β)} {x y z : β}, y ∈ UniformSpace.ball x V → z ∈ UniformSpace.ball y W → z ∈ UniformSpace.ball x (compRel V W) This theorem, named `mem_ball_comp`, states the triangle inequality for `UniformSpace.ball` in a uniform space. More specifically, it states that for any type `β`, and any sets `V, W` of type `(β × β)`, and any elements `x, y, z` of type `β`, if `y` is in the ball centered at `x` with respect to `V` and `z` is in the ball centered at `y` with respect to `W`, then `z` is in the ball centered at `x` with respect to the composition of the relations `V` and `W`. It's a generalization of the triangle inequality from metric spaces to uniform spaces. More concisely: If `x, y, z` are elements of a uniform space, and the balls centered at `x` with respect to relation `V` and at `y` with respect to relation `W` both contain `z`, then `z` is in the ball centered at `x` with respect to the composition of `V` and `W`.
`Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq` theorem Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {r : Set (α × α)} {s : Set β} {f g : β → α}, (∀ x ∈ s, ContinuousAt f x) → (∀ x ∈ s, ContinuousAt g x) → Set.EqOn f g s → r ∈ uniformity α → ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r This theorem states that given two functions `f` and `g` from a topological space `β` to a uniform space `α`, which are both continuous on a set `s` and coincide on this set, and given a relation `r` (a set of pairs of points in `α`) that is in the uniformity of `α`, there exists an open set `t` which contains `s` such that for every point `x` in `t`, the pair `(f x, g x)` is in the relation `r`. In other words, if two continuous functions agree on a set, then they are "uniformly close" on some open neighborhood of that set, where "uniformly close" is defined according to the uniform structure on the codomain. More concisely: Given continuous functions `f` and `g` from a topological space `β` to a uniform space `α` that agree on a set `s`, there exists an open set `t` containing `s` such that `(f x, g x)` is in the uniformity relation `r` for all `x` in `t`.
`eventually_uniformity_comp_subset` theorem eventually_uniformity_comp_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set (α × α)}, s ∈ uniformity α → ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, compRel t t ⊆ s This theorem states that for any type `α` with a uniform space structure and any set of pairs `s` from `α`, if `s` belongs to the uniformity of `α`, then there is a point in the future (eventually) of the filter of small sets of the uniformity of `α` where, for any subset `t` of these small sets, the composition of relations of `t` with itself is a subset of `s`. In other words, if we take a sufficiently small set `t` from the uniformity of `α`, then pairs consisting of elements that can both be reached from some element of `t` through this relation, must be in `s`. More concisely: For any uniform space `α` and subset `s` of its uniformity, if `s` is an element of the uniformity, then there exists a small set `t` such that the composition of relations of `t` with itself is contained in `s`.
`Dense.biUnion_uniformity_ball` theorem Dense.biUnion_uniformity_ball : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α} {U : Set (α × α)}, Dense s → U ∈ uniformity α → ⋃ x ∈ s, UniformSpace.ball x U = Set.univ This theorem states that for any type `α` with a uniform space structure, any set `s` of `α`, and any set `U` of pairs of `α`, if `s` is dense and `U` belongs to the uniformity of `α`, then the union of all uniform balls centered at points in `s` with respect to `U` covers the entire space `α` (i.e., equals the universal set on `α`). In simpler terms, it says that every point in the space can be found within some uniform ball centered at a point in `s`, assuming `s` is dense and `U` is a set within the uniformity of the space. This theorem is a key result in topology and it helps to understand the structure of dense sets in uniform spaces. More concisely: Given a uniform space `(α, U)`, a dense set `s ∈ U`, any point `x ∈ α` lies in some uniform ball centered at a point in `s`.
`discreteTopology_of_discrete_uniformity` theorem discreteTopology_of_discrete_uniformity : ∀ {α : Type ua} [hα : UniformSpace α], uniformity α = Filter.principal idRel → DiscreteTopology α This theorem states that for any type `α` that has a uniform space structure, if the uniformity of `α` is equal to the principal filter of the identity relation, then `α` has a discrete topology. In other words, if all the "closeness" information in a space is described by the simplest possible relation - the identity - then the topology of the space is discrete, meaning that every subset of the space is open. More concisely: If the uniformity of a uniform space `α` is equal to its identity relation, then `α` has a discrete topology.
`Mathlib.Topology.UniformSpace.Basic._auxLemma.24` theorem Mathlib.Topology.UniformSpace.Basic._auxLemma.24 : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ}, Filter.Tendsto f a (Filter.comap g c) = Filter.Tendsto (g ∘ f) a c This theorem, `Mathlib.Topology.UniformSpace.Basic._auxLemma.24`, states that for all types `α`, `β`, `γ`, all functions `f` from `α` to `β` and `g` from `β` to `γ`, and all filters `a` on `α` and `c` on `γ`, the condition that `f` tends towards the preimage filter of `g` under `c` when filtered by `a` is equivalent to the condition that the composition of `g` and `f` tends towards `c` when filtered by `a`. In other words, we have commutativity of function composition and filter transformation in the context of the limit of a function. More concisely: For filters `a` on a type `α`, `c` on a type `γ`, functions `f: α → β`, and `g: β → γ`, the filters `f''^(-1)'[c]` and `(g ∘ f)''[a]` are equal if and only if `f` tends towards the preimage of `g` under `c` when filtered by `a`, and `g` tends towards `c` when filtered by `a`.
`comp_mem_uniformity_sets` theorem comp_mem_uniformity_sets : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set (α × α)}, s ∈ uniformity α → ∃ t ∈ uniformity α, compRel t t ⊆ s This theorem states that for any type `α` equipped with a UniformSpace structure and for any set `s` of pairs of `α`, if `s` is a member of the uniformity filter of `α`, then there exists another set `t` in the uniformity filter such that the composition of relations `t` with itself is a subset of `s`. In other words, if `s` is a set of "sufficiently close" pairs in our uniform space, we can find another set of "sufficiently close" pairs `t` such that for any pair in `t`, there's a "middle" element making this pair and another pair in `t` "close" in the sense of belonging to `s`. More concisely: Given a UniformSpace `α` and a set `s` of pairwise `α × α` in its uniformity filter, there exists a set `t` in the uniformity filter such that `t` is closed under composition with itself and is contained in `s`.
`Monotone.compRel` theorem Monotone.compRel : ∀ {α : Type ua} {β : Type ub} [inst : Preorder β] {f g : β → Set (α × α)}, Monotone f → Monotone g → Monotone fun x => compRel (f x) (g x) This theorem states that for any type `α` and any preordered type `β`, if we have two functions `f` and `g` from `β` to the set of ordered pairs of `α`, then if both `f` and `g` are monotone functions, the function that maps `x` to the composition of the relations `f(x)` and `g(x)` is also monotone. In other words, the monotonicity is preserved under the composition of relations. More concisely: If `f` and `g` are monotone functions from a preordered type `β` to the ordered pairs of a type `α`, then their composition `f ∘ g` is also a monotone function.
`refl_le_uniformity` theorem refl_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.principal idRel ≤ uniformity α The theorem `refl_le_uniformity` states that for any type `α` equipped with a uniform space structure, the principal filter of the identity relation (`idRel`), which consists of all sets containing pairs `(x, x)` for some `x` in `α`, is a subset of the uniformity of `α`. In other words, every set in the uniformity of `α` contains all pairs of identical elements from `α`. This theorem provides a condition that is always satisfied by the uniformity in any uniform space. More concisely: In any uniform space, the principal filter of the identity relation is included in the uniformity.
`uniformity_comap` theorem uniformity_comap : ∀ {α : Type ua} {β : Type ub} {x : UniformSpace β} (f : α → β), uniformity α = Filter.comap (Prod.map f f) (uniformity β) The theorem `uniformity_comap` states that for any types `α` and `β`, given a uniform space structure `x` on `β` and a function `f` from `α` to `β`, the uniformity filter on `α` is equivalent to the pre-image of the uniformity filter on `β` under the function `Prod.map f f`. Here, `Prod.map f f` is a function that applies `f` to both elements of a pair from `α × α` and maps it to `β × β`. In essence, this theorem relates the uniform structures of two spaces when a function is known to exist between them. More concisely: For any uniform spaces (α, ς\_α) and (β, ς\_β), and any function f : α → β, the pre-image filter of the uniformity filter ς\_β on β under f is equivalent to the uniformity filter ENDOR\_α(f) on α.
`prod_mk_mem_compRel` theorem prod_mk_mem_compRel : ∀ {α : Type ua} {a b c : α} {s t : Set (α × α)}, (a, c) ∈ s → (c, b) ∈ t → (a, b) ∈ compRel s t This theorem states that for any type `α` and any three elements `a`, `b`, and `c` of type `α`, and any two sets `s` and `t` of pairs of elements of type `α`, if the pair `(a, c)` belongs to the set `s` and the pair `(c, b)` belongs to the set `t`, then the pair `(a, b)` belongs to the composition of the relations `s` and `t`. The composition of relations `s` and `t` is defined as the set of all pairs `(x, y)` such that there exists some `z` where `(x, z)` is in `s` and `(z, y)` is in `t`. More concisely: If `(a, c)` is in the relation `s` and `(c, b)` is in the relation `t`, then `(a, b)` is in the composition of `s` and `t`.
`isOpen_iff_ball_subset` theorem isOpen_iff_ball_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α}, IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ uniformity α, UniformSpace.ball x V ⊆ s This theorem states that for any type `α` that has a `UniformSpace` structure and any set `s` of type `α`, the set `s` is open if and only if for every element `x` in `s`, there exists a set `V` in the uniformity of `α` such that the ball centered at `x` with respect to `V` is a subset of `s`. In the context of topology, the "ball" around a point `x` is a set of points that are "close" to `x` according to some definition of closeness (given by `V`). This theorem is thus an alternative characterization of open sets in terms of uniform spaces. More concisely: A set of a type `α` with a `UniformSpace` structure is open if and only if for each of its element `x`, there exists a set `V` in the uniformity of `α` such that the ball centered at `x` with respect to `V` is contained in the set.
`uniformity_hasBasis_closed` theorem uniformity_hasBasis_closed : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsClosed V) id := by sorry This theorem states that for any type `α` which has a `UniformSpace` structure, the uniformity on `α` has a basis given by a certain property. Specifically, the basis sets for the uniformity are those sets `V` that belong to the uniformity and are also closed. Here, `Filter.HasBasis` is a concept from filter theory in topology, which describes when a filter is generated by a certain collection of sets. The `id` function in the theorem signifies that the sets themselves are used as a basis, not some function of the sets. More concisely: For any uniform space `(α, U)` with type `α`, the basis of its uniformity `U` is given by the closed sets belonging to `U`.
`symmetrizeRel_subset_self` theorem symmetrizeRel_subset_self : ∀ {α : Type ua} (V : Set (α × α)), symmetrizeRel V ⊆ V This theorem states that for any type `α` and any set `V` of pairs of elements of type `α`, the symmetrized version of `V` is a subset of `V` itself. Here, "symmetrizing" a set of pairs means taking the intersection of the set with the set of pairs obtained by swapping the elements in each pair from the original set. In mathematical terms, given a set of ordered pairs `(a, b)`, its symmetrized version contains pairs `(a, b)` and `(b, a)` as long as both pairs are in the original set `V`. More concisely: For any set `V` of pairs of elements from type `α`, the symmetrized version of `V` (i.e., `V` intersect the set of swapped pairs) is a subset of `V`.

LeanAide GPT-4 documentation

Module: Mathlib.Topology.UniformSpace.Basic

uniformity_eq_symm

theorem uniformity_eq_symm : ∀ {α : Type ua} [inst : UniformSpace α], uniformity α = Prod.swap <$> uniformity α := by sorry

UniformSpace.le_sInf

theorem UniformSpace.le_sInf : ∀ {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α}, (∀ t' ∈ tt, t ≤ t') → t ≤ sInf tt

mem_nhds_left

theorem mem_nhds_left : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) {s : Set (α × α)}, s ∈ uniformity α → {y | (x, y) ∈ s} ∈ nhds x

Mathlib.Topology.UniformSpace.Basic._auxLemma.1

theorem Mathlib.Topology.UniformSpace.Basic._auxLemma.1 : ∀ {α : Type ua} {a b : α}, ((a, b) ∈ idRel) = (a = b) := by sorry

symm_le_uniformity

theorem symm_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.map Prod.swap (uniformity α) ≤ uniformity α

mem_nhds_uniformity_iff_right

theorem mem_nhds_uniformity_iff_right : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ {p | p.1 = x → p.2 ∈ s} ∈ uniformity α

AddOpposite.uniformContinuous_unop

theorem AddOpposite.uniformContinuous_unop : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous AddOpposite.unop

uniformContinuous_inf_dom_right₂

theorem uniformContinuous_inf_dom_right₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}, (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2

lebesgue_number_of_compact_open

theorem lebesgue_number_of_compact_open : ∀ {α : Type ua} [inst : UniformSpace α] {K U : Set α}, IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ uniformity α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U

UniformSpace.Core.comp

theorem UniformSpace.Core.comp : ∀ {α : Type u} (self : UniformSpace.Core α), (self.uniformity.lift' fun s => compRel s s) ≤ self.uniformity := by sorry

UniformContinuous.subtype_mk

theorem UniformContinuous.subtype_mk : ∀ {α : Type ua} {β : Type ub} {p : α → Prop} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (h : ∀ (x : β), p (f x)), UniformContinuous fun x => ⟨f x, ⋯⟩

compRel_mono

theorem compRel_mono : ∀ {α : Type ua} {f g h k : Set (α × α)}, f ⊆ h → g ⊆ k → compRel f g ⊆ compRel h k

eventually_uniformity_iterate_comp_subset

theorem eventually_uniformity_iterate_comp_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set (α × α)}, s ∈ uniformity α → ∀ (n : ℕ), ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, (fun x => compRel t x)^[n] t ⊆ s

tendsto_diag_uniformity

theorem tendsto_diag_uniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] (f : β → α) (l : Filter β), Filter.Tendsto (fun x => (f x, f x)) l (uniformity α)

UniformSpace.comap_iInf

theorem UniformSpace.comap_iInf : ∀ {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ι → UniformSpace γ} {f : α → γ}, UniformSpace.comap f (⨅ i, u i) = ⨅ i, UniformSpace.comap f (u i)

nhdsSet_diagonal_le_uniformity

theorem nhdsSet_diagonal_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], nhdsSet (Set.diagonal α) ≤ uniformity α

uniformContinuous_of_const

theorem uniformContinuous_of_const : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {c : α → β}, (∀ (a b : α), c a = c b) → UniformContinuous c

uniformContinuousOn_iff_restrict

theorem uniformContinuousOn_iff_restrict : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α}, UniformContinuousOn f s ↔ UniformContinuous (s.restrict f)

uniformity_prod_eq_prod

theorem uniformity_prod_eq_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], uniformity (α × β) = Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)

uniformity_hasBasis_closure

theorem uniformity_hasBasis_closure : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α) closure

tendsto_swap_uniformity

theorem tendsto_swap_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.Tendsto Prod.swap (uniformity α) (uniformity α)

comp_le_uniformity3

theorem comp_le_uniformity3 : ∀ {α : Type ua} [inst : UniformSpace α], ((uniformity α).lift' fun s => compRel s (compRel s s)) ≤ uniformity α

uniformContinuous_const

theorem uniformContinuous_const : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {b : β}, UniformContinuous fun x => b

MulOpposite.uniformContinuous_unop

theorem MulOpposite.uniformContinuous_unop : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous MulOpposite.unop

Filter.HasBasis.uniformContinuous_iff

nhds_le_uniformity

theorem nhds_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] (x : α), nhds (x, x) ≤ uniformity α

UniformSpace.ext

theorem UniformSpace.ext : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, uniformity α = uniformity α → u₁ = u₂

UniformSpace.hasBasis_nhds

theorem UniformSpace.hasBasis_nhds : ∀ {α : Type ua} [inst : UniformSpace α] (x : α), (nhds x).HasBasis (fun s => s ∈ uniformity α ∧ SymmetricRel s) fun s => UniformSpace.ball x s

UniformContinuous.prod_map

uniformity_prod

theorem uniformity_prod : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], uniformity (α × β) = Filter.comap (fun p => (p.1.1, p.2.1)) (uniformity α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (uniformity β)

uniformContinuous_inf_dom_left₂

theorem uniformContinuous_inf_dom_left₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}, (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2

uniformContinuous_snd

theorem uniformContinuous_snd : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun p => p.2

Uniform.tendsto_nhds_right

theorem Uniform.tendsto_nhds_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : Filter β} {u : β → α} {a : α}, Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (a, u x)) f (uniformity α)

UniformSpace.hasBasis_symmetric

theorem UniformSpace.hasBasis_symmetric : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun s => s ∈ uniformity α ∧ SymmetricRel s) id

uniformContinuous_sInf_dom₂

uniformity_hasBasis_open_symmetric

theorem uniformity_hasBasis_open_symmetric : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V ∧ SymmetricRel V) id

symmetric_symmetrizeRel

theorem symmetric_symmetrizeRel : ∀ {α : Type ua} (V : Set (α × α)), SymmetricRel (symmetrizeRel V)

UniformSpace.Core.refl

theorem UniformSpace.Core.refl : ∀ {α : Type u} (self : UniformSpace.Core α), Filter.principal idRel ≤ self.uniformity

union_mem_uniformity_sum

Uniform.tendsto_nhds_left

theorem Uniform.tendsto_nhds_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {f : Filter β} {u : β → α} {a : α}, Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (u x, a)) f (uniformity α)

uniformContinuous_fst

theorem uniformContinuous_fst : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun p => p.1

`uniformity_eq_symm`

`UniformSpace.le_sInf`

`mem_nhds_left`

`Mathlib.Topology.UniformSpace.Basic._auxLemma.1`

`symm_le_uniformity`

`mem_nhds_uniformity_iff_right`

`AddOpposite.uniformContinuous_unop`

`uniformContinuous_inf_dom_right₂`

`lebesgue_number_of_compact_open`

`UniformSpace.Core.comp`

`UniformContinuous.subtype_mk`

`compRel_mono`

`eventually_uniformity_iterate_comp_subset`

`tendsto_diag_uniformity`

`UniformSpace.comap_iInf`

`nhdsSet_diagonal_le_uniformity`

`uniformContinuous_of_const`

`uniformContinuousOn_iff_restrict`

`uniformity_prod_eq_prod`

`uniformity_hasBasis_closure`

`tendsto_swap_uniformity`

`comp_le_uniformity3`

`uniformContinuous_const`

`MulOpposite.uniformContinuous_unop`

`Filter.HasBasis.uniformContinuous_iff`

`nhds_le_uniformity`

`UniformSpace.ext`

`UniformSpace.hasBasis_nhds`

`UniformContinuous.prod_map`

`uniformity_prod`

`uniformContinuous_inf_dom_left₂`

`uniformContinuous_snd`

`Uniform.tendsto_nhds_right`

`UniformSpace.hasBasis_symmetric`

`uniformContinuous_sInf_dom₂`

`uniformity_hasBasis_open_symmetric`

`symmetric_symmetrizeRel`

`UniformSpace.Core.refl`

`union_mem_uniformity_sum`

`Uniform.tendsto_nhds_left`

`uniformContinuous_fst`

`uniformity_prod_eq_comap_prod`

`subset_comp_self`

`nhds_eq_comap_uniformity`

`comap_swap_uniformity`

`comp_le_uniformity`

`Filter.HasBasis.mem_uniformity_iff`

`uniformContinuous_id`

`nhds_eq_uniformity`

`symmetrize_mem_uniformity`

`uniformContinuous_comap`

`uniformity_hasBasis_open`

`UniformSpace.toTopologicalSpace_iInf`

`UniformSpace.ball_mem_nhds`

`nhds_basis_uniformity'`

`uniformContinuous_comap'`

`Filter.Tendsto.uniformity_symm`

`UniformSpace.comap_comap`

`idRel_subset`

`Filter.Tendsto.uniformity_trans`

`UniformContinuous.comp`

`iSup_nhds_le_uniformity`

`UniformSpace.ofCoreEq_toCore`

`iInf_uniformity`

`UniformSpace.Core.symm`

`ball_mono`

`uniformContinuousOn_univ`

`UniformContinuous.continuous`

`uniformContinuous_subtype_val`

`UniformSpace.hasBasis_ofFun`

`lebesgue_number_lemma`

`comp_symm_mem_uniformity_sets`

`nhds_basis_uniformity`

`lebesgue_number_lemma_sUnion`