Mathlib.Topology.UniformSpace.Defs

idRel definition

{α : Type*}

Full source

/-- The identity relation, or the graph of the identity function -/
def idRel {α : Type*} :=
  { p : α × α | p.1 = p.2 }

Identity relation

Informal description

The identity relation on a type $\alpha$ is the set $\{(x, x) \mid x \in \alpha\}$ consisting of all pairs where both elements are equal. In other words, it is the graph of the identity function on $\alpha$.

mem_idRel theorem

{a b : α} : (a, b) ∈ @idRel α ↔ a = b

Full source

@[simp]
theorem mem_idRel {a b : α} : (a, b)(a, b) ∈ @idRel α(a, b) ∈ @idRel α ↔ a = b :=
  Iff.rfl

Characterization of Identity Relation: $(a, b) \in \text{idRel} \leftrightarrow a = b$

Informal description

For any elements $a$ and $b$ of a type $\alpha$, the pair $(a, b)$ belongs to the identity relation $\text{idRel}$ if and only if $a = b$.

idRel_subset theorem

{s : Set (α × α)} : idRel ⊆ s ↔ ∀ a, (a, a) ∈ s

Full source

@[simp]
theorem idRel_subset {s : Set (α × α)} : idRelidRel ⊆ sidRel ⊆ s ↔ ∀ a, (a, a) ∈ s := by
  simp [subset_def]

Subset Characterization of Identity Relation: $\text{idRel} \subseteq s \leftrightarrow \forall a, (a, a) \in s$

Informal description

For any set $s$ of pairs in $\alpha \times \alpha$, the identity relation $\text{idRel}$ is a subset of $s$ if and only if for every element $a \in \alpha$, the pair $(a, a)$ belongs to $s$.

compRel definition

(r₁ r₂ : Set (α × α))

Full source

/-- The composition of relations -/
def compRel (r₁ r₂ : Set (α × α)) :=
  { p : α × α | ∃ z : α, (p.1, z) ∈ r₁ ∧ (z, p.2) ∈ r₂ }

Composition of relations

Informal description

Given two relations $ r_1, r_2 $ on $ \alpha \times \alpha $, their composition $ r_1 \circ r_2 $ is the set of all pairs $(x, z)$ such that there exists an intermediate element $ y $ with $(x, y) \in r_1$ and $(y, z) \in r_2$. This operation abstracts the triangle inequality in metric spaces and the continuity of addition in topological groups.

Uniformity.term_○_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped[Uniformity] infixl:62 " ○ " => compRel

Composition of relations in uniform spaces

Informal description

The notation `○` represents the composition of relations in the context of uniform spaces. Given two relations `r₁` and `r₂` on a type `α × α`, their composition `r₁ ○ r₂` is defined as the set of all pairs `(x, z)` such that there exists an intermediate element `y` with `(x, y) ∈ r₁` and `(y, z) ∈ r₂`. This operation is used to abstract the triangle inequality in metric spaces and the continuity of addition in topological groups.

mem_compRel theorem

 {α : Type u} {r₁ r₂ : Set (α × α)} {x y : α} : (x, y) ∈ r₁ ○ r₂ ↔ ∃ z, (x, z) ∈ r₁ ∧ (z, y) ∈ r₂

Full source

@[simp]
theorem mem_compRel {α : Type u} {r₁ r₂ : Set (α × α)} {x y : α} :
    (x, y)(x, y) ∈ r₁ ○ r₂(x, y) ∈ r₁ ○ r₂ ↔ ∃ z, (x, z) ∈ r₁ ∧ (z, y) ∈ r₂ :=
  Iff.rfl

Characterization of Relation Composition: $(x, y) \in r_1 \circ r_2 \leftrightarrow \exists z, (x, z) \in r_1 \land (z, y) \in r_2$

Informal description

For any type $\alpha$ and relations $r_1, r_2$ on $\alpha \times \alpha$, the pair $(x, y)$ belongs to the composition $r_1 \circ r_2$ if and only if there exists an intermediate element $z$ such that $(x, z) \in r_1$ and $(z, y) \in r_2$.

swap_idRel theorem

: Prod.swap '' idRel = @idRel α

Full source

@[simp]
theorem swap_idRel : Prod.swapProd.swap '' idRel = @idRel α :=
  Set.ext fun ⟨a, b⟩ => by simpa [image_swap_eq_preimage_swap] using eq_comm

Invariance of Identity Relation under Swap: $\text{swap}'' \text{idRel} = \text{idRel}$

Informal description

The image of the identity relation under the swap operation (which exchanges the components of each pair) is equal to the identity relation itself. In other words, swapping the components of all pairs in the set $\{(x, x) \mid x \in \alpha\}$ leaves the set unchanged.

Monotone.compRel theorem

[Preorder β] {f g : β → Set (α × α)} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ○ g x

Full source

theorem Monotone.compRel [Preorder β] {f g : β → Set (α × α)} (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x => f x ○ g x := fun _ _ h _ ⟨z, h₁, h₂⟩ => ⟨z, hf h h₁, hg h h₂⟩

Monotonicity of Relation Composition under Monotone Functions

Informal description

Let $\beta$ be a preorder and $f, g \colon \beta \to \mathcal{P}(\alpha \times \alpha)$ be monotone functions. Then the function $x \mapsto f(x) \circ g(x)$, where $\circ$ denotes the composition of relations, is also monotone.

compRel_mono theorem

{f g h k : Set (α × α)} (h₁ : f ⊆ h) (h₂ : g ⊆ k) : f ○ g ⊆ h ○ k

Full source

@[mono, gcongr]
theorem compRel_mono {f g h k : Set (α × α)} (h₁ : f ⊆ h) (h₂ : g ⊆ k) : f ○ gf ○ g ⊆ h ○ k :=
  fun _ ⟨z, h, h'⟩ => ⟨z, h₁ h, h₂ h'⟩

Monotonicity of Relation Composition: $f \subseteq h \land g \subseteq k \Rightarrow f \circ g \subseteq h \circ k$

Informal description

For any relations $f, g, h, k$ on $\alpha \times \alpha$, if $f \subseteq h$ and $g \subseteq k$, then the composition $f \circ g$ is a subset of the composition $h \circ k$.

prodMk_mem_compRel theorem

{a b c : α} {s t : Set (α × α)} (h₁ : (a, c) ∈ s) (h₂ : (c, b) ∈ t) : (a, b) ∈ s ○ t

Full source

theorem prodMk_mem_compRel {a b c : α} {s t : Set (α × α)} (h₁ : (a, c)(a, c) ∈ s) (h₂ : (c, b)(c, b) ∈ t) :
    (a, b)(a, b) ∈ s ○ t :=
  ⟨c, h₁, h₂⟩

Membership in Relation Composition: $(a, b) \in s \circ t$ given $(a, c) \in s$ and $(c, b) \in t$

Informal description

For any elements $a, b, c$ in a type $\alpha$ and relations $s, t$ on $\alpha \times \alpha$, if $(a, c) \in s$ and $(c, b) \in t$, then $(a, b) \in s \circ t$, where $\circ$ denotes the composition of relations.

id_compRel theorem

{r : Set (α × α)} : idRel ○ r = r

Full source

@[simp]
theorem id_compRel {r : Set (α × α)} : idRelidRel ○ r = r :=
  Set.ext fun ⟨a, b⟩ => by simp

Identity Relation is Left Neutral for Composition: $\text{idRel} \circ r = r$

Informal description

For any relation $r$ on $\alpha \times \alpha$, the composition of the identity relation with $r$ equals $r$, i.e., $\text{idRel} \circ r = r$.

compRel_assoc theorem

{r s t : Set (α × α)} : r ○ s ○ t = r ○ (s ○ t)

Full source

theorem compRel_assoc {r s t : Set (α × α)} : r ○ sr ○ s ○ t = r ○ (s ○ t) := by
  ext ⟨a, b⟩; simp only [mem_compRel]; tauto

Associativity of Relation Composition

Informal description

For any three relations $ r, s, t $ on $ \alpha \times \alpha $, the composition of relations is associative, i.e., $ (r \circ s) \circ t = r \circ (s \circ t) $.

left_subset_compRel theorem

{s t : Set (α × α)} (h : idRel ⊆ t) : s ⊆ s ○ t

Full source

theorem left_subset_compRel {s t : Set (α × α)} (h : idRelidRel ⊆ t) : s ⊆ s ○ t := fun ⟨_x, y⟩ xy_in =>
  ⟨y, xy_in, h <| rfl⟩

Inclusion of Relation in its Composition when Identity is Contained: $s \subseteq s \circ t$ if $\text{idRel} \subseteq t$

Informal description

For any relations $s$ and $t$ on $\alpha \times \alpha$, if the identity relation $\text{idRel}$ is contained in $t$, then $s$ is contained in the composition $s \circ t$.

right_subset_compRel theorem

{s t : Set (α × α)} (h : idRel ⊆ s) : t ⊆ s ○ t

Full source

theorem right_subset_compRel {s t : Set (α × α)} (h : idRelidRel ⊆ s) : t ⊆ s ○ t := fun ⟨x, _y⟩ xy_in =>
  ⟨x, h <| rfl, xy_in⟩

Inclusion of Relation in Composition with Identity-Containing Relation

Informal description

For any relations $ s $ and $ t $ on $ \alpha \times \alpha $, if the identity relation is contained in $ s $, then $ t $ is contained in the composition $ s \circ t $.

subset_comp_self theorem

{s : Set (α × α)} (h : idRel ⊆ s) : s ⊆ s ○ s

Full source

theorem subset_comp_self {s : Set (α × α)} (h : idRelidRel ⊆ s) : s ⊆ s ○ s :=
  left_subset_compRel h

Self-composition containment for identity-containing relations: $s \subseteq s \circ s$ when $\text{idRel} \subseteq s$

Informal description

For any relation $s$ on $\alpha \times \alpha$ that contains the identity relation (i.e., $\text{idRel} \subseteq s$), the relation $s$ is contained in its composition with itself (i.e., $s \subseteq s \circ s$).

subset_iterate_compRel theorem

{s t : Set (α × α)} (h : idRel ⊆ s) (n : ℕ) : t ⊆ (s ○ ·)^[n] t

Full source

theorem subset_iterate_compRel {s t : Set (α × α)} (h : idRelidRel ⊆ s) (n : ℕ) :
    t ⊆ (s ○ ·)^[n] t := by
  induction n generalizing t with
  | zero => exact Subset.rfl
  | succ n ihn => exact (right_subset_compRel h).trans ihn

Iterated Composition Contains Relation: $t \subseteq (s \circ \cdot)^n t$ when $\text{idRel} \subseteq s$

Informal description

For any relations $s$ and $t$ on $\alpha \times \alpha$ such that the identity relation is contained in $s$ (i.e., $\text{idRel} \subseteq s$), and for any natural number $n$, the relation $t$ is contained in the $n$-th iterate of the composition operation with $s$ applied to $t$ (i.e., $t \subseteq (s \circ \cdot)^{[n]} t$).

IsSymmetricRel definition

(V : Set (α × α)) : Prop

Full source

/-- The relation is invariant under swapping factors. -/
def IsSymmetricRel (V : Set (α × α)) : Prop :=
  Prod.swapProd.swap ⁻¹' V = V

Symmetric relation

Informal description

A relation $ V $ on $ \alpha \times \alpha $ is called symmetric if it is invariant under swapping the factors, i.e., $ (x, y) \in V $ if and only if $ (y, x) \in V $.

symmetrizeRel definition

(V : Set (α × α)) : Set (α × α)

Full source

/-- The maximal symmetric relation contained in a given relation. -/
def symmetrizeRel (V : Set (α × α)) : Set (α × α) :=
  V ∩ Prod.swap ⁻¹' V

Symmetrization of a relation

Informal description

Given a relation $ V $ on $ \alpha \times \alpha $, the symmetrization of $ V $ is the intersection of $ V $ with its inverse under the swap operation, i.e., $ V \cap \{(y, x) \mid (x, y) \in V\} $. This results in the largest symmetric relation contained in $ V $.

symmetric_symmetrizeRel theorem

(V : Set (α × α)) : IsSymmetricRel (symmetrizeRel V)

Full source

theorem symmetric_symmetrizeRel (V : Set (α × α)) : IsSymmetricRel (symmetrizeRel V) := by
  simp [IsSymmetricRel, symmetrizeRel, preimage_inter, inter_comm, ← preimage_comp]

Symmetry of the Symmetrization of a Relation

Informal description

For any relation $V$ on $\alpha \times \alpha$, the symmetrization of $V$ is symmetric, i.e., $(x, y) \in \text{symmetrizeRel}(V)$ if and only if $(y, x) \in \text{symmetrizeRel}(V)$.

symmetrizeRel_subset_self theorem

(V : Set (α × α)) : symmetrizeRel V ⊆ V

Full source

theorem symmetrizeRel_subset_self (V : Set (α × α)) : symmetrizeRelsymmetrizeRel V ⊆ V :=
  sep_subset _ _

Symmetrization is a Subset of the Original Relation

Informal description

For any relation $ V $ on $ \alpha \times \alpha $, the symmetrization of $ V $ is a subset of $ V $, i.e., $\text{symmetrizeRel}(V) \subseteq V$.

symmetrize_mono theorem

{V W : Set (α × α)} (h : V ⊆ W) : symmetrizeRel V ⊆ symmetrizeRel W

Full source

@[mono]
theorem symmetrize_mono {V W : Set (α × α)} (h : V ⊆ W) : symmetrizeRelsymmetrizeRel V ⊆ symmetrizeRel W :=
  inter_subset_inter h <| preimage_mono h

Monotonicity of Relation Symmetrization: $ V \subseteq W $ implies $ \text{symmetrizeRel}(V) \subseteq \text{symmetrizeRel}(W) $

Informal description

For any two relations $ V $ and $ W $ on $ \alpha \times \alpha $, if $ V \subseteq W $, then the symmetrization of $ V $ is contained in the symmetrization of $ W $. In other words, the symmetrization operation is monotone with respect to the subset relation.

IsSymmetricRel.mk_mem_comm theorem

{V : Set (α × α)} (hV : IsSymmetricRel V) {x y : α} : (x, y) ∈ V ↔ (y, x) ∈ V

Full source

theorem IsSymmetricRel.mk_mem_comm {V : Set (α × α)} (hV : IsSymmetricRel V) {x y : α} :
    (x, y)(x, y) ∈ V(x, y) ∈ V ↔ (y, x) ∈ V :=
  Set.ext_iff.1 hV (y, x)

Characterization of Symmetric Relations: $(x, y) \in V \leftrightarrow (y, x) \in V$

Informal description

For any symmetric relation $ V $ on $ \alpha \times \alpha $ and any elements $ x, y \in \alpha $, we have $(x, y) \in V$ if and only if $(y, x) \in V$.

IsSymmetricRel.eq theorem

{U : Set (α × α)} (hU : IsSymmetricRel U) : Prod.swap ⁻¹' U = U

Full source

theorem IsSymmetricRel.eq {U : Set (α × α)} (hU : IsSymmetricRel U) : Prod.swapProd.swap ⁻¹' U = U :=
  hU

Preimage of Symmetric Relation Under Swap Equals Itself

Informal description

For any symmetric relation $ U $ on $ \alpha \times \alpha $, the preimage of $ U $ under the swap operation $ \text{swap} : \alpha \times \alpha \to \alpha \times \alpha $ is equal to $ U $ itself, i.e., $ \text{swap}^{-1}(U) = U $.

IsSymmetricRel.inter theorem

{U V : Set (α × α)} (hU : IsSymmetricRel U) (hV : IsSymmetricRel V) : IsSymmetricRel (U ∩ V)

Full source

theorem IsSymmetricRel.inter {U V : Set (α × α)} (hU : IsSymmetricRel U) (hV : IsSymmetricRel V) :
    IsSymmetricRel (U ∩ V) := by rw [IsSymmetricRel, preimage_inter, hU.eq, hV.eq]

Intersection of Symmetric Relations is Symmetric

Informal description

For any two symmetric relations $U$ and $V$ on $\alpha \times \alpha$, their intersection $U \cap V$ is also a symmetric relation.

IsSymmetricRel.iInter theorem

{U : (i : ι) → Set (α × α)} (hU : ∀ i, IsSymmetricRel (U i)) : IsSymmetricRel (⋂ i, U i)

Full source

theorem IsSymmetricRel.iInter {U : (i : ι) → Set (α × α)} (hU : ∀ i, IsSymmetricRel (U i)) :
    IsSymmetricRel (⋂ i, U i) := by
  simp_rw [IsSymmetricRel, preimage_iInter, (hU _).eq]

Intersection of Symmetric Relations is Symmetric

Informal description

For any indexed family of relations $\{U_i\}_{i \in \iota}$ on $\alpha \times \alpha$ where each $U_i$ is symmetric, the intersection $\bigcap_{i} U_i$ is also symmetric. That is, if $(x, y) \in \bigcap_{i} U_i$ implies $(y, x) \in \bigcap_{i} U_i$ for all $x, y \in \alpha$.

IsSymmetricRel.sInter theorem

{s : Set (Set (α × α))} (h : ∀ i ∈ s, IsSymmetricRel i) : IsSymmetricRel (⋂₀ s)

Full source

lemma IsSymmetricRel.sInter {s : Set (Set (α × α))} (h : ∀ i ∈ s, IsSymmetricRel i) :
    IsSymmetricRel (⋂₀ s) := by
  rw [sInter_eq_iInter]
  exact IsSymmetricRel.iInter (by simpa)

Intersection of Symmetric Relations is Symmetric

Informal description

For any family of relations $\{U_i\}_{i \in s}$ on $\alpha \times \alpha$ where each $U_i$ is symmetric (i.e., $(x, y) \in U_i$ implies $(y, x) \in U_i$ for all $x, y \in \alpha$), the intersection $\bigcap_{i \in s} U_i$ is also symmetric.

IsSymmetricRel.preimage_prodMap theorem

{U : Set (β × β)} (ht : IsSymmetricRel U) (f : α → β) : IsSymmetricRel (Prod.map f f ⁻¹' U)

Full source

lemma IsSymmetricRel.preimage_prodMap {U : Set (β × β)} (ht : IsSymmetricRel U) (f : α → β) :
    IsSymmetricRel (Prod.mapProd.map f f ⁻¹' U) :=
  Set.ext fun _ ↦ ht.mk_mem_comm

Preimage of Symmetric Relation under Product Map is Symmetric

Informal description

Let $U$ be a symmetric relation on $\beta \times \beta$ (i.e., $(x, y) \in U$ if and only if $(y, x) \in U$ for all $x, y \in \beta$). Then for any function $f : \alpha \to \beta$, the preimage of $U$ under the product map $f \times f$ (i.e., $\{(x, y) \mid (f(x), f(y)) \in U\}$) is also a symmetric relation on $\alpha \times \alpha$.

UniformSpace.Core structure

(α : Type u)

Full source

/-- This core description of a uniform space is outside of the type class hierarchy. It is useful
  for constructions of uniform spaces, when the topology is derived from the uniform space. -/
structure UniformSpace.Core (α : Type u) where
  /-- The uniformity filter. Once `UniformSpace` is defined, `𝓤 α` (`_root_.uniformity`) becomes the
  normal form. -/
  uniformity : Filter (α × α)
  /-- Every set in the uniformity filter includes the diagonal. -/
  refl : 𝓟 idRel ≤ uniformity
  /-- If `s ∈ uniformity`, then `Prod.swap ⁻¹' s ∈ uniformity`. -/
  symm : Tendsto Prod.swap uniformity uniformity
  /-- For every set `u ∈ uniformity`, there exists `v ∈ uniformity` such that `v ○ v ⊆ u`. -/
  comp : (uniformity.lift' fun s => s ○ s) ≤ uniformity

Uniform Space Core

Informal description

A uniform space core on a type $\alpha$ consists of a filter $\mathcal{U}$ on $\alpha \times \alpha$ (called the uniformity) satisfying three conditions: 1. **Reflexivity:** Every entourage $V \in \mathcal{U}$ contains the diagonal $\{(x, x) \mid x \in \alpha\}$. 2. **Symmetry:** For every entourage $V \in \mathcal{U}$, the inverse relation $\{(y, x) \mid (x, y) \in V\}$ is also in $\mathcal{U}$. 3. **Triangle inequality:** For every entourage $V \in \mathcal{U}$, there exists an entourage $W \in \mathcal{U}$ such that the composition $W \circ W \subseteq V$, where $W \circ W = \{(x, z) \mid \exists y, (x, y) \in W \text{ and } (y, z) \in W\}$. This structure is used to construct uniform spaces when the topology is derived from the uniformity.

UniformSpace.Core.comp_mem_uniformity_sets theorem

{c : Core α} {s : Set (α × α)} (hs : s ∈ c.uniformity) : ∃ t ∈ c.uniformity, t ○ t ⊆ s

Full source

protected theorem UniformSpace.Core.comp_mem_uniformity_sets {c : Core α} {s : Set (α × α)}
    (hs : s ∈ c.uniformity) : ∃ t ∈ c.uniformity, t ○ t ⊆ s :=
  (mem_lift'_sets <| monotone_id.compRel monotone_id).mp <| c.comp hs

Existence of Compositional Entourage in Uniform Space Core

Informal description

For any uniform space core $c$ on a type $\alpha$ and any entourage $s \in c.\text{uniformity}$, there exists another entourage $t \in c.\text{uniformity}$ such that the composition $t \circ t$ is contained in $s$.

UniformSpace.Core.mk' definition

 {α : Type u} (U : Filter (α × α)) (refl : ∀ r ∈ U, ∀ (x), (x, x) ∈ r) (symm : ∀ r ∈ U, Prod.swap ⁻¹' r ∈ U)
  (comp : ∀ r ∈ U, ∃ t ∈ U, t ○ t ⊆ r) : UniformSpace.Core α

Full source

/-- An alternative constructor for `UniformSpace.Core`. This version unfolds various
`Filter`-related definitions. -/
def UniformSpace.Core.mk' {α : Type u} (U : Filter (α × α)) (refl : ∀ r ∈ U, ∀ (x), (x, x) ∈ r)
    (symm : ∀ r ∈ U, Prod.swap ⁻¹' r ∈ U) (comp : ∀ r ∈ U, ∃ t ∈ U, t ○ t ⊆ r) :
    UniformSpace.Core α :=
  ⟨U, fun _r ru => idRel_subset.2 (refl _ ru), symm, fun _r ru =>
    let ⟨_s, hs, hsr⟩ := comp _ ru
    mem_of_superset (mem_lift' hs) hsr⟩

Uniform Space Core Constructor from Filter Conditions

Informal description

Given a type $\alpha$ and a filter $U$ on $\alpha \times \alpha$ satisfying: 1. **Reflexivity:** For every relation $r \in U$ and every $x \in \alpha$, the pair $(x, x)$ belongs to $r$ 2. **Symmetry:** For every relation $r \in U$, the inverse relation $\{(y, x) \mid (x, y) \in r\}$ is also in $U$ 3. **Triangle inequality:** For every relation $r \in U$, there exists $t \in U$ such that the composition $t \circ t \subseteq r$ this constructs a uniform space core structure on $\alpha$ with uniformity $U$.

UniformSpace.Core.mkOfBasis definition

 {α : Type u} (B : FilterBasis (α × α)) (refl : ∀ r ∈ B, ∀ (x), (x, x) ∈ r)
  (symm : ∀ r ∈ B, ∃ t ∈ B, t ⊆ Prod.swap ⁻¹' r) (comp : ∀ r ∈ B, ∃ t ∈ B, t ○ t ⊆ r) : UniformSpace.Core α

Full source

/-- Defining a `UniformSpace.Core` from a filter basis satisfying some uniformity-like axioms. -/
def UniformSpace.Core.mkOfBasis {α : Type u} (B : FilterBasis (α × α))
    (refl : ∀ r ∈ B, ∀ (x), (x, x) ∈ r) (symm : ∀ r ∈ B, ∃ t ∈ B, t ⊆ Prod.swap ⁻¹' r)
    (comp : ∀ r ∈ B, ∃ t ∈ B, t ○ t ⊆ r) : UniformSpace.Core α where
  uniformity := B.filter
  refl := B.hasBasis.ge_iff.mpr fun _r ru => idRel_subset.2 <| refl _ ru
  symm := (B.hasBasis.tendsto_iff B.hasBasis).mpr symm
  comp := (HasBasis.le_basis_iff (B.hasBasis.lift' (monotone_id.compRel monotone_id))
    B.hasBasis).2 comp

Uniform space core from a basis satisfying reflexivity, symmetry, and triangle inequality

Informal description

Given a filter basis $ B $ on $ \alpha \times \alpha $ satisfying the following conditions: 1. **Reflexivity:** For every $ r \in B $ and every $ x \in \alpha $, the pair $(x, x)$ is in $ r $. 2. **Symmetry:** For every $ r \in B $, there exists $ t \in B $ such that $ t $ is contained in the inverse relation of $ r $, i.e., $ t \subseteq \{(y, x) \mid (x, y) \in r\} $. 3. **Triangle inequality:** For every $ r \in B $, there exists $ t \in B $ such that the composition $ t \circ t $ is contained in $ r $. The function constructs a uniform space core on $ \alpha $ where the uniformity filter is generated by $ B $. This core satisfies the standard uniform space axioms derived from the given basis.

UniformSpace.Core.toTopologicalSpace definition

{α : Type u} (u : UniformSpace.Core α) : TopologicalSpace α

Full source

/-- A uniform space generates a topological space -/
def UniformSpace.Core.toTopologicalSpace {α : Type u} (u : UniformSpace.Core α) :
    TopologicalSpace α :=
  .mkOfNhds fun x ↦ .comap (Prod.mk x) u.uniformity

Topology induced by a uniform space core

Informal description

Given a uniform space core structure `u` on a type `α`, the function constructs the induced topological space on `α` where the neighborhood filter at each point `x` is defined as the preimage of the uniformity filter under the map `y ↦ (x, y)`.

UniformSpace.Core.ext theorem

: ∀ {u₁ u₂ : UniformSpace.Core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂

Full source

theorem UniformSpace.Core.ext :
    ∀ {u₁ u₂ : UniformSpace.Core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

Equality of Uniform Space Cores via Uniformity Filters

Informal description

For any two uniform space cores $u_1$ and $u_2$ on a type $\alpha$, if their uniformity filters are equal ($\mathcal{U}_1 = \mathcal{U}_2$), then $u_1 = u_2$.

UniformSpace.Core.nhds_toTopologicalSpace theorem

{α : Type u} (u : Core α) (x : α) : @nhds α u.toTopologicalSpace x = comap (Prod.mk x) u.uniformity

Full source

theorem UniformSpace.Core.nhds_toTopologicalSpace {α : Type u} (u : Core α) (x : α) :
    @nhds α u.toTopologicalSpace x = comap (Prod.mk x) u.uniformity := by
  apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun _ ↦ (basis_sets _).comap _)
  · exact fun a U hU ↦ u.refl hU rfl
  · intro a U hU
    rcases u.comp_mem_uniformity_sets hU with ⟨V, hV, hVU⟩
    filter_upwards [preimage_mem_comap hV] with b hb
    filter_upwards [preimage_mem_comap hV] with c hc
    exact hVU ⟨b, hb, hc⟩

Neighborhood Filter Characterization in Uniform Space Core

Informal description

For any uniform space core $u$ on a type $\alpha$ and any point $x \in \alpha$, the neighborhood filter at $x$ in the topology induced by $u$ is equal to the preimage of the uniformity filter under the map $y \mapsto (x, y)$. In other words, $\mathcal{N}(x) = \text{comap}\, (y \mapsto (x, y))\, \mathcal{U}$, where $\mathcal{N}(x)$ is the neighborhood filter at $x$ and $\mathcal{U}$ is the uniformity filter of $u$.

UniformSpace structure

(α : Type u) extends TopologicalSpace α

Full source

/-- A uniform space is a generalization of the "uniform" topological aspects of a
  metric space. It consists of a filter on `α × α` called the "uniformity", which
  satisfies properties analogous to the reflexivity, symmetry, and triangle properties
  of a metric.

  A metric space has a natural uniformity, and a uniform space has a natural topology.
  A topological group also has a natural uniformity, even when it is not metrizable. -/
class UniformSpace (α : Type u) extends TopologicalSpace α where
  /-- The uniformity filter. -/
  protected uniformity : Filter (α × α)
  /-- If `s ∈ uniformity`, then `Prod.swap ⁻¹' s ∈ uniformity`. -/
  protected symm : Tendsto Prod.swap uniformity uniformity
  /-- For every set `u ∈ uniformity`, there exists `v ∈ uniformity` such that `v ○ v ⊆ u`. -/
  protected comp : (uniformity.lift' fun s => s ○ s) ≤ uniformity
  /-- The uniformity agrees with the topology: the neighborhoods filter of each point `x`
  is equal to `Filter.comap (Prod.mk x) (𝓤 α)`. -/
  protected nhds_eq_comap_uniformity (x : α) : 𝓝 x = comap (Prod.mk x) uniformity

Uniform Space Structure

Informal description

A uniform space structure on a type $\alpha$ consists of a filter on $\alpha \times \alpha$ called the *uniformity*, which generalizes the notion of uniform closeness in metric spaces. The uniformity must satisfy three key properties analogous to those of a metric: 1. Reflexivity: Every entourage contains the diagonal $\{(x,x) \mid x \in \alpha\}$. 2. Symmetry: For every entourage $V$, there exists a symmetric entourage $W$ such that $W \subseteq V$. 3. Triangle inequality: For every entourage $V$, there exists an entourage $W$ such that the composition $W \circ W \subseteq V$. This structure induces a natural topology on $\alpha$ where neighborhoods are determined by the uniformity. The uniformity captures uniform continuity and other uniform notions that generalize from metric spaces and topological groups.

uniformity definition

(α : Type u) [UniformSpace α] : Filter (α × α)

Full source

/-- The uniformity is a filter on α × α (inferred from an ambient uniform space
  structure on α). -/
def uniformity (α : Type u) [UniformSpace α] : Filter (α × α) :=
  @UniformSpace.uniformity α _

Uniformity filter of a uniform space

Informal description

For a uniform space $\alpha$, the uniformity is a filter on $\alpha \times \alpha$ that captures the notion of uniform closeness between points. This filter, denoted $\mathfrak{U}(\alpha)$, consists of entourages that satisfy: 1. Reflexivity: Every entourage contains the diagonal $\{(x,x) \mid x \in \alpha\}$ 2. Symmetry: For every entourage $V$, there exists a symmetric entourage $W$ such that $W \subseteq V$ 3. Triangle inequality: For every entourage $V$, there exists an entourage $W$ such that the composition $W \circ W \subseteq V$

Uniformity.term𝓤[_] definition

: Lean.ParserDescr✝

Full source

/-- Notation for the uniformity filter with respect to a non-standard `UniformSpace` instance. -/
scoped[Uniformity] notation "𝓤[" u "]" => @uniformity _ u

Uniformity filter notation for non-standard uniform spaces

Informal description

The notation `𝓤[ u ]` represents the uniformity filter on a type with respect to a non-standard uniform space structure `u`.

Uniformity.term𝓤 definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped[Uniformity] notation "𝓤" => uniformity

Uniformity filter notation

Informal description

The notation `𝓤 X` represents the uniformity filter on a uniform space `X`, which consists of entourages that capture the notion of "closeness" in the space.

UniformSpace.ofCoreEq abbrev

{α : Type u} (u : UniformSpace.Core α) (t : TopologicalSpace α) (h : t = u.toTopologicalSpace) : UniformSpace α

Full source

/-- Construct a `UniformSpace` from a `u : UniformSpace.Core` and a `TopologicalSpace` structure
that is equal to `u.toTopologicalSpace`. -/
abbrev UniformSpace.ofCoreEq {α : Type u} (u : UniformSpace.Core α) (t : TopologicalSpace α)
    (h : t = u.toTopologicalSpace) : UniformSpace α where
  __ := u
  toTopologicalSpace := t
  nhds_eq_comap_uniformity x := by rw [h, u.nhds_toTopologicalSpace]

Uniform Space Construction from Core with Specified Topology

Informal description

Given a uniform space core structure `u` on a type `α` and a topological space structure `t` on `α` such that `t` is equal to the topology induced by `u`, this constructs a uniform space structure on `α` where the uniformity is given by `u` and the topology is `t`.

UniformSpace.ofCore abbrev

{α : Type u} (u : UniformSpace.Core α) : UniformSpace α

Full source

/-- Construct a `UniformSpace` from a `UniformSpace.Core`. -/
abbrev UniformSpace.ofCore {α : Type u} (u : UniformSpace.Core α) : UniformSpace α :=
  .ofCoreEq u _ rfl

Construction of Uniform Space from Core Structure

Informal description

Given a uniform space core structure $u$ on a type $\alpha$, this constructs a uniform space on $\alpha$ where the uniformity is given by $u$ and the topology is induced by $u$.

UniformSpace.toCore abbrev

(u : UniformSpace α) : UniformSpace.Core α

Full source

/-- Construct a `UniformSpace.Core` from a `UniformSpace`. -/
abbrev UniformSpace.toCore (u : UniformSpace α) : UniformSpace.Core α where
  __ := u
  refl := by
    rintro U hU ⟨x, y⟩ (rfl : x = y)
    have : Prod.mkProd.mk x ⁻¹' UProd.mk x ⁻¹' U ∈ 𝓝 x := by
      rw [UniformSpace.nhds_eq_comap_uniformity]
      exact preimage_mem_comap hU
    convert mem_of_mem_nhds this

Extraction of Uniform Space Core from Uniform Space

Informal description

Given a uniform space structure on a type $\alpha$, the function `UniformSpace.toCore` extracts the underlying uniform space core, which consists of the uniformity filter on $\alpha \times \alpha$ satisfying the reflexivity, symmetry, and triangle inequality conditions.

UniformSpace.toCore_toTopologicalSpace theorem

(u : UniformSpace α) : u.toCore.toTopologicalSpace = u.toTopologicalSpace

Full source

theorem UniformSpace.toCore_toTopologicalSpace (u : UniformSpace α) :
    u.toCore.toTopologicalSpace = u.toTopologicalSpace :=
  TopologicalSpace.ext_nhds fun a ↦ by
    rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

Equality of Topologies Induced by Uniform Space Core and Uniform Space

Informal description

For any uniform space structure $u$ on a type $\alpha$, the topology induced by the core uniformity of $u$ is equal to the topology of $u$.

UniformSpace.mem_uniformity_ofCore_iff theorem

{u : UniformSpace.Core α} {s : Set (α × α)} : s ∈ 𝓤[.ofCore u] ↔ s ∈ u.uniformity

Full source

lemma UniformSpace.mem_uniformity_ofCore_iff {u : UniformSpace.Core α} {s : Set (α × α)} :
    s ∈ 𝓤[.ofCore u]s ∈ 𝓤[.ofCore u] ↔ s ∈ u.uniformity :=
  Iff.rfl

Equivalence of Uniformity Filters in Core Construction

Informal description

For a uniform space core structure $u$ on a type $\alpha$ and a set $s \subseteq \alpha \times \alpha$, the set $s$ belongs to the uniformity filter of the uniform space constructed from $u$ if and only if $s$ belongs to the uniformity filter of $u$.

UniformSpace.ext theorem

{u₁ u₂ : UniformSpace α} (h : 𝓤[u₁] = 𝓤[u₂]) : u₁ = u₂

Full source

@[ext (iff := false)]
protected theorem UniformSpace.ext {u₁ u₂ : UniformSpace α} (h : 𝓤[u₁] = 𝓤[u₂]) : u₁ = u₂ := by
  have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
    rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
    exact congr_arg (comap _) h
  cases u₁; cases u₂; congr

Uniform Space Equality Criterion via Uniformity Filters

Informal description

Two uniform space structures on a type $\alpha$ are equal if their uniformity filters $\mathfrak{U}(\alpha)$ coincide.

UniformSpace.ext_iff theorem

{u₁ u₂ : UniformSpace α} : u₁ = u₂ ↔ ∀ s, s ∈ 𝓤[u₁] ↔ s ∈ 𝓤[u₂]

Full source

protected theorem UniformSpace.ext_iff {u₁ u₂ : UniformSpace α} :
    u₁ = u₂ ↔ ∀ s, s ∈ 𝓤[u₁] ↔ s ∈ 𝓤[u₂] :=
  ⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩

Uniform Space Equality Criterion via Uniformity Filters

Informal description

Two uniform space structures $u_1$ and $u_2$ on a type $\alpha$ are equal if and only if for every set $s \subseteq \alpha \times \alpha$, $s$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$ of $u_1$ if and only if it belongs to the uniformity filter of $u_2$.

UniformSpace.ofCoreEq_toCore theorem

(u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace) : .ofCoreEq u.toCore t h = u

Full source

theorem UniformSpace.ofCoreEq_toCore (u : UniformSpace α) (t : TopologicalSpace α)
    (h : t = u.toCore.toTopologicalSpace) : .ofCoreEq u.toCore t h = u :=
  UniformSpace.ext rfl

Uniform Space Construction from Core Preserves Original Structure

Informal description

Given a uniform space structure $u$ on a type $\alpha$ and a topological space structure $t$ on $\alpha$ such that $t$ is equal to the topology induced by the core of $u$, the uniform space constructed from the core of $u$ with topology $t$ is equal to $u$.

UniformSpace.replaceTopology abbrev

{α : Type*} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace) : UniformSpace α

Full source

/-- Replace topology in a `UniformSpace` instance with a propositionally (but possibly not
definitionally) equal one. -/
abbrev UniformSpace.replaceTopology {α : Type*} [i : TopologicalSpace α] (u : UniformSpace α)
    (h : i = u.toTopologicalSpace) : UniformSpace α where
  __ := u
  toTopologicalSpace := i
  nhds_eq_comap_uniformity x := by rw [h, u.nhds_eq_comap_uniformity]

Uniform Space with Replaced Topology

Informal description

Given a uniform space structure on a type $\alpha$ with a topology $i$, and a proof $h$ that $i$ is equal to the topology induced by the uniform structure, the operation `UniformSpace.replaceTopology` constructs a new uniform space structure on $\alpha$ with the same uniformity but with the topology replaced by $i$.

UniformSpace.replaceTopology_eq theorem

{α : Type*} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace) : u.replaceTopology h = u

Full source

theorem UniformSpace.replaceTopology_eq {α : Type*} [i : TopologicalSpace α] (u : UniformSpace α)
    (h : i = u.toTopologicalSpace) : u.replaceTopology h = u :=
  UniformSpace.ext rfl

Uniform Space Replacement of Topology Preserves Original Structure

Informal description

Given a uniform space structure $u$ on a type $\alpha$ with a topology $i$, and a proof $h$ that $i$ is equal to the topology induced by $u$, the operation `replaceTopology` returns the original uniform space structure $u$.

nhds_eq_comap_uniformity theorem

{x : α} : 𝓝 x = (𝓤 α).comap (Prod.mk x)

Full source

theorem nhds_eq_comap_uniformity {x : α} : 𝓝 x = (𝓤 α).comap (Prod.mk x) :=
  UniformSpace.nhds_eq_comap_uniformity x

Neighborhood Filter as Uniformity Preimage

Informal description

For any point $x$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ is equal to the preimage of the uniformity filter $\mathfrak{U}(\alpha)$ under the map $y \mapsto (x, y)$.

isOpen_uniformity theorem

{s : Set α} : IsOpen s ↔ ∀ x ∈ s, {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Full source

theorem isOpen_uniformity {s : Set α} :
    IsOpenIsOpen s ↔ ∀ x ∈ s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α := by
  simp only [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap_prodMk]

Characterization of Open Sets via Uniformity

Informal description

A subset $s$ of a uniform space $\alpha$ is open if and only if for every point $x \in s$, the set $\{(x', y) \in \alpha \times \alpha \mid x' = x \implies y \in s\}$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$.

refl_le_uniformity theorem

: 𝓟 idRel ≤ 𝓤 α

Full source

theorem refl_le_uniformity : 𝓟 idRel ≤ 𝓤 α :=
  (@UniformSpace.toCore α _).refl

Reflexivity of Uniformity: $\text{idRel} \subseteq \mathfrak{U}(\alpha)$

Informal description

The identity relation $\text{idRel} = \{(x, x) \mid x \in \alpha\}$ is contained in every entourage of the uniformity filter $\mathfrak{U}(\alpha)$ on a uniform space $\alpha$. In other words, the principal filter generated by the identity relation is finer than the uniformity filter.

uniformity.neBot instance

[Nonempty α] : NeBot (𝓤 α)

Full source

instance uniformity.neBot [Nonempty α] : NeBot (𝓤 α) :=
  diagonal_nonempty.principal_neBot.mono refl_le_uniformity

Non-triviality of Uniformity Filter on Nonempty Uniform Spaces

Informal description

For any nonempty uniform space $\alpha$, the uniformity filter $\mathfrak{U}(\alpha)$ is nonempty and does not contain the empty set.

refl_mem_uniformity theorem

{x : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) : (x, x) ∈ s

Full source

theorem refl_mem_uniformity {x : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) : (x, x)(x, x) ∈ s :=
  refl_le_uniformity h rfl

Reflexivity in Uniform Spaces: $(x, x) \in s$ for all $x$ and entourages $s$

Informal description

For any uniform space $\alpha$, any entourage $s \in \mathfrak{U}(\alpha)$, and any point $x \in \alpha$, the pair $(x, x)$ belongs to $s$.

mem_uniformity_of_eq theorem

{x y : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) (hx : x = y) : (x, y) ∈ s

Full source

theorem mem_uniformity_of_eq {x y : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) (hx : x = y) : (x, y)(x, y) ∈ s :=
  refl_le_uniformity h hx

Diagonal Membership in Entourages

Informal description

For any points $x$ and $y$ in a uniform space $\alpha$, and any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$, if $x = y$ then $(x, y) \in s$.

symm_le_uniformity theorem

: map (@Prod.swap α α) (𝓤 _) ≤ 𝓤 _

Full source

theorem symm_le_uniformity : map (@Prod.swap α α) (𝓤 _) ≤ 𝓤 _ :=
  UniformSpace.symm

Symmetry Property of Uniformity Filter

Informal description

For any uniform space $\alpha$, the filter obtained by applying the swap operation $(x, y) \mapsto (y, x)$ to the uniformity filter $\mathfrak{U}(\alpha)$ is contained in $\mathfrak{U}(\alpha)$ itself. In other words, if $V$ is an entourage in the uniformity, then $\{(y, x) \mid (x, y) \in V\}$ is also an entourage.

comp_le_uniformity theorem

: ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) ≤ 𝓤 α

Full source

theorem comp_le_uniformity : ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) ≤ 𝓤 α :=
  UniformSpace.comp

Triangle Inequality for Uniformity Filter

Informal description

For any uniform space $\alpha$, the filter generated by compositions of entourages from the uniformity filter $\mathfrak{U}(\alpha)$ is contained in $\mathfrak{U}(\alpha)$ itself. That is, for any entourage $V \in \mathfrak{U}(\alpha)$, there exists an entourage $W \in \mathfrak{U}(\alpha)$ such that the composition $W \circ W \subseteq V$.

lift'_comp_uniformity theorem

: ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) = 𝓤 α

Full source

theorem lift'_comp_uniformity : ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) = 𝓤 α :=
  comp_le_uniformity.antisymm <| le_lift'.2 fun _s hs ↦ mem_of_superset hs <|
    subset_comp_self <| idRel_subset.2 fun _ ↦ refl_mem_uniformity hs

Uniformity Filter Equals Its Composition Closure: $\mathfrak{U}(\alpha) = \text{lift}' (\circ) \mathfrak{U}(\alpha)$

Informal description

For any uniform space $\alpha$, the filter generated by compositions of entourages from the uniformity filter $\mathfrak{U}(\alpha)$ is equal to $\mathfrak{U}(\alpha)$ itself. That is, the filter $\mathfrak{U}(\alpha)$ is closed under composition of entourages.

tendsto_swap_uniformity theorem

: Tendsto (@Prod.swap α α) (𝓤 α) (𝓤 α)

Full source

theorem tendsto_swap_uniformity : Tendsto (@Prod.swap α α) (𝓤 α) (𝓤 α) :=
  symm_le_uniformity

Uniformity Filter is Preserved Under Swap

Informal description

For any uniform space $\alpha$, the function $\text{swap} : \alpha \times \alpha \to \alpha \times \alpha$ defined by $(x, y) \mapsto (y, x)$ is a uniform map with respect to the uniformity filter $\mathfrak{U}(\alpha)$. That is, the image of any entourage under swap remains an entourage.

comp_mem_uniformity_sets theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ t ⊆ s

Full source

theorem comp_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ t ⊆ s :=
  (mem_lift'_sets <| monotone_id.compRel monotone_id).mp <| comp_le_uniformity hs

Existence of Composition-Refining Entourage in Uniformity Filter

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, there exists another entourage $t \in \mathfrak{U}(\alpha)$ such that the composition $t \circ t$ is contained in $s$.

Filter.Tendsto.uniformity_trans theorem

 {l : Filter β} {f₁ f₂ f₃ : β → α} (h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α))
  (h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)) : Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α)

Full source

/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is transitive. -/
theorem Filter.Tendsto.uniformity_trans {l : Filter β} {f₁ f₂ f₃ : β → α}
    (h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α))
    (h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)) : Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α) := by
  refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity
  filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩

Transitivity of Uniform Convergence

Informal description

Let $\alpha$ be a uniform space and $\beta$ be a type with a filter $l$. For any three functions $f_1, f_2, f_3 : \beta \to \alpha$, if the pairs $(f_1(x), f_2(x))$ and $(f_2(x), f_3(x))$ tend to the uniformity $\mathfrak{U}(\alpha)$ as $x$ tends along $l$, then the pair $(f_1(x), f_3(x))$ also tends to $\mathfrak{U}(\alpha)$ along $l$.

Filter.Tendsto.uniformity_symm theorem

{l : Filter β} {f : β → α × α} (h : Tendsto f l (𝓤 α)) : Tendsto (fun x => ((f x).2, (f x).1)) l (𝓤 α)

Full source

/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is symmetric. -/
theorem Filter.Tendsto.uniformity_symm {l : Filter β} {f : β → α × α} (h : Tendsto f l (𝓤 α)) :
    Tendsto (fun x => ((f x).2, (f x).1)) l (𝓤 α) :=
  tendsto_swap_uniformity.comp h

Symmetry of Uniform Convergence

Informal description

For any filter $l$ on a type $\beta$ and any function $f : \beta \to \alpha \times \alpha$, if the pair $(f(x).1, f(x).2)$ tends to the uniformity $\mathfrak{U}(\alpha)$ as $x$ tends along $l$, then the pair $(f(x).2, f(x).1)$ also tends to $\mathfrak{U}(\alpha)$ along $l$.

tendsto_diag_uniformity theorem

(f : β → α) (l : Filter β) : Tendsto (fun x => (f x, f x)) l (𝓤 α)

Full source

/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is reflexive. -/
theorem tendsto_diag_uniformity (f : β → α) (l : Filter β) :
    Tendsto (fun x => (f x, f x)) l (𝓤 α) := fun _s hs =>
  mem_map.2 <| univ_mem' fun _ => refl_mem_uniformity hs

Reflexivity of Uniform Convergence: $(f(x), f(x)) \to \mathfrak{U}(\alpha)$ along $l$

Informal description

For any function $f \colon \beta \to \alpha$ from a type $\beta$ with a filter $l$ to a uniform space $\alpha$, the pair $(f(x), f(x))$ tends to the uniformity $\mathfrak{U}(\alpha)$ as $x$ tends along $l$.

tendsto_const_uniformity theorem

{a : α} {f : Filter β} : Tendsto (fun _ => (a, a)) f (𝓤 α)

Full source

theorem tendsto_const_uniformity {a : α} {f : Filter β} : Tendsto (fun _ => (a, a)) f (𝓤 α) :=
  tendsto_diag_uniformity (fun _ => a) f

Constant Pair Convergence to Uniformity

Informal description

For any point $a$ in a uniform space $\alpha$ and any filter $f$ on a type $\beta$, the constant function mapping every element of $\beta$ to the pair $(a, a)$ tends to the uniformity $\mathfrak{U}(\alpha)$ along $f$.

symm_of_uniformity theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, (∀ a b, (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s

Full source

theorem symm_of_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, (∀ a b, (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s :=
  have : preimagepreimage Prod.swap s ∈ 𝓤 α := symm_le_uniformity hs
  ⟨s ∩ preimage Prod.swap s, inter_mem hs this, fun _ _ ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩, inter_subset_left⟩

Existence of Symmetric Entourage in Uniformity Filter

Informal description

For any uniform space $\alpha$ and any entourage $s \in \mathfrak{U}(\alpha)$, there exists a symmetric entourage $t \in \mathfrak{U}(\alpha)$ such that $t \subseteq s$. Here, symmetry means that for any $a, b \in \alpha$, if $(a, b) \in t$ then $(b, a) \in t$.

comp_symm_of_uniformity theorem

 {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, (∀ {a b}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s

Full source

theorem comp_symm_of_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, (∀ {a b}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s :=
  let ⟨_t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
  let ⟨t', ht', ht'₁, ht'₂⟩ := symm_of_uniformity ht₁
  ⟨t', ht', ht'₁ _ _, Subset.trans (monotone_id.compRel monotone_id ht'₂) ht₂⟩

Existence of Symmetric Entourage with Composition Refinement in Uniformity Filter

Informal description

For any uniform space $\alpha$ and any entourage $s \in \mathfrak{U}(\alpha)$, there exists a symmetric entourage $t \in \mathfrak{U}(\alpha)$ such that: 1. For all $a, b \in \alpha$, if $(a, b) \in t$ then $(b, a) \in t$ (symmetry) 2. The composition $t \circ t \subseteq s$ (triangle inequality refinement)

uniformity_le_symm theorem

: 𝓤 α ≤ @Prod.swap α α <$> 𝓤 α

Full source

theorem uniformity_le_symm : 𝓤 α ≤ @Prod.swap α α <$> 𝓤 α := by
  rw [map_swap_eq_comap_swap]; exact tendsto_swap_uniformity.le_comap

Uniformity Filter is Finer than its Swap Image

Informal description

For any uniform space $\alpha$, the uniformity filter $\mathfrak{U}(\alpha)$ is finer than the image of itself under the swap operation $(x, y) \mapsto (y, x)$. In other words, for every entourage $V \in \mathfrak{U}(\alpha)$, there exists an entourage $W \in \mathfrak{U}(\alpha)$ such that $(y, x) \in V$ whenever $(x, y) \in W$.

uniformity_eq_symm theorem

: 𝓤 α = @Prod.swap α α <$> 𝓤 α

Full source

theorem uniformity_eq_symm : 𝓤 α = @Prod.swap α α <$> 𝓤 α :=
  le_antisymm uniformity_le_symm symm_le_uniformity

Symmetry of Uniformity Filter: $\mathfrak{U}(\alpha) = \text{swap}(\mathfrak{U}(\alpha))$

Informal description

For any uniform space $\alpha$, the uniformity filter $\mathfrak{U}(\alpha)$ is equal to its image under the swap operation $(x, y) \mapsto (y, x)$. That is, $\mathfrak{U}(\alpha) = \{(y, x) \mid (x, y) \in \mathfrak{U}(\alpha)\}$.

comap_swap_uniformity theorem

: comap (@Prod.swap α α) (𝓤 α) = 𝓤 α

Full source

@[simp]
theorem comap_swap_uniformity : comap (@Prod.swap α α) (𝓤 α) = 𝓤 α :=
  (congr_arg _ uniformity_eq_symm).trans <| comap_map Prod.swap_injective

Uniformity Filter Invariance Under Swap: $\text{comap}(\text{swap}, \mathfrak{U}(\alpha)) = \mathfrak{U}(\alpha)$

Informal description

For any uniform space $\alpha$, the preimage of the uniformity filter $\mathfrak{U}(\alpha)$ under the swap operation $(x, y) \mapsto (y, x)$ is equal to $\mathfrak{U}(\alpha)$ itself. In other words, $\text{comap}(\text{swap}, \mathfrak{U}(\alpha)) = \mathfrak{U}(\alpha)$.

symmetrize_mem_uniformity theorem

{V : Set (α × α)} (h : V ∈ 𝓤 α) : symmetrizeRel V ∈ 𝓤 α

Full source

theorem symmetrize_mem_uniformity {V : Set (α × α)} (h : V ∈ 𝓤 α) : symmetrizeRelsymmetrizeRel V ∈ 𝓤 α := by
  apply (𝓤 α).inter_sets h
  rw [← image_swap_eq_preimage_swap, uniformity_eq_symm]
  exact image_mem_map h

Symmetrization of an Entourage is an Entourage

Informal description

For any entourage $V$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, the symmetrization of $V$ (defined as $V \cap \{(y, x) \mid (x, y) \in V\}$) is also an entourage in $\mathfrak{U}(\alpha)$.

UniformSpace.hasBasis_symmetric theorem

: (𝓤 α).HasBasis (fun s : Set (α × α) => s ∈ 𝓤 α ∧ IsSymmetricRel s) id

Full source

/-- Symmetric entourages form a basis of `𝓤 α` -/
theorem UniformSpace.hasBasis_symmetric :
    (𝓤 α).HasBasis (fun s : Set (α × α) => s ∈ 𝓤 αs ∈ 𝓤 α ∧ IsSymmetricRel s) id :=
  hasBasis_self.2 fun t t_in =>
    ⟨symmetrizeRel t, symmetrize_mem_uniformity t_in, symmetric_symmetrizeRel t,
      symmetrizeRel_subset_self t⟩

Existence of Symmetric Entourage Basis in Uniform Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ has a basis consisting of symmetric entourages. That is, for any entourage $V \in \mathfrak{U}(\alpha)$, there exists a symmetric entourage $W \in \mathfrak{U}(\alpha)$ such that $W \subseteq V$.

uniformity_lift_le_swap theorem

 {g : Set (α × α) → Filter β} {f : Filter β} (hg : Monotone g)
  (h : ((𝓤 α).lift fun s => g (preimage Prod.swap s)) ≤ f) : (𝓤 α).lift g ≤ f

Full source

theorem uniformity_lift_le_swap {g : Set (α × α) → Filter β} {f : Filter β} (hg : Monotone g)
    (h : ((𝓤 α).lift fun s => g (preimage Prod.swap s)) ≤ f) : (𝓤 α).lift g ≤ f :=
  calc
    (𝓤 α).lift g ≤ (Filter.map (@Prod.swap α α) <| 𝓤 α).lift g :=
      lift_mono uniformity_le_symm le_rfl
    _ ≤ _ := by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h

Lifted Uniformity Filter under Swap Preimage is Finer

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$, and let $\beta$ be another type. For any monotone function $g : \text{Set}(\alpha \times \alpha) \to \text{Filter}(\beta)$ and any filter $f$ on $\beta$, if the lifted filter $\mathfrak{U}(\alpha).\text{lift}(s \mapsto g(\text{preimage}(\text{swap}, s)))$ is finer than $f$, then the lifted filter $\mathfrak{U}(\alpha).\text{lift}(g)$ is also finer than $f$. Here, $\text{swap} : \alpha \times \alpha \to \alpha \times \alpha$ is the function $(x, y) \mapsto (y, x)$.

uniformity_lift_le_comp theorem

{f : Set (α × α) → Filter β} (h : Monotone f) : ((𝓤 α).lift fun s => f (s ○ s)) ≤ (𝓤 α).lift f

Full source

theorem uniformity_lift_le_comp {f : Set (α × α) → Filter β} (h : Monotone f) :
    ((𝓤 α).lift fun s => f (s ○ s)) ≤ (𝓤 α).lift f :=
  calc
    ((𝓤 α).lift fun s => f (s ○ s)) = ((𝓤 α).lift' fun s : Set (α × α) => s ○ s).lift f := by
      rw [lift_lift'_assoc]
      · exact monotone_id.compRel monotone_id
      · exact h
    _ ≤ (𝓤 α).lift f := lift_mono comp_le_uniformity le_rfl

Monotone Lift of Composition over Uniformity Filter

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$, and let $\beta$ be a type. For any monotone function $f \colon \mathcal{P}(\alpha \times \alpha) \to \text{Filter}(\beta)$, the filter generated by lifting $f$ over compositions of entourages is contained in the filter generated by lifting $f$ directly over the uniformity. That is, \[ \left( \mathfrak{U}(\alpha) \right).\text{lift} \left( \lambda s, f(s \circ s) \right) \leq \left( \mathfrak{U}(\alpha) \right).\text{lift} f. \]

comp3_mem_uniformity theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s

Full source

theorem comp3_mem_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s :=
  let ⟨_t', ht', ht's⟩ := comp_mem_uniformity_sets hs
  let ⟨t, ht, htt'⟩ := comp_mem_uniformity_sets ht'
  ⟨t, ht, (compRel_mono ((subset_comp_self (refl_le_uniformity ht)).trans htt') htt').trans ht's⟩

Existence of Triple Composition-Refining Entourage in Uniformity Filter

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, there exists another entourage $t \in \mathfrak{U}(\alpha)$ such that the triple composition $t \circ (t \circ t)$ is contained in $s$.

comp_le_uniformity3 theorem

: ((𝓤 α).lift' fun s : Set (α × α) => s ○ (s ○ s)) ≤ 𝓤 α

Full source

/-- See also `comp3_mem_uniformity`. -/
theorem comp_le_uniformity3 : ((𝓤 α).lift' fun s : Set (α × α) => s ○ (s ○ s)) ≤ 𝓤 α := fun _ h =>
  let ⟨_t, htU, ht⟩ := comp3_mem_uniformity h
  mem_of_superset (mem_lift' htU) ht

Triple Composition of Entourages is Contained in Uniformity Filter

Informal description

For any uniform space $\alpha$ with uniformity filter $\mathfrak{U}(\alpha)$, the filter generated by the triple composition of entourages is contained in the uniformity filter. That is, \[ \left( \mathfrak{U}(\alpha) \right).\text{lift}' \left( \lambda s, s \circ (s \circ s) \right) \leq \mathfrak{U}(\alpha). \]

comp_symm_mem_uniformity_sets theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsSymmetricRel t ∧ t ○ t ⊆ s

Full source

/-- See also `comp_open_symm_mem_uniformity_sets`. -/
theorem comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, IsSymmetricRel t ∧ t ○ t ⊆ s := by
  obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
  use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w
  have : symmetrizeRelsymmetrizeRel w ⊆ w := symmetrizeRel_subset_self w
  calc symmetrizeRel w ○ symmetrizeRel w
    _ ⊆ w ○ wcalc symmetrizeRel w ○ symmetrizeRel w
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s     := w_sub

Existence of Symmetric Entourage with Composition-Refinement Property

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, there exists a symmetric entourage $t \in \mathfrak{U}(\alpha)$ such that the composition $t \circ t$ is contained in $s$.

subset_comp_self_of_mem_uniformity theorem

{s : Set (α × α)} (h : s ∈ 𝓤 α) : s ⊆ s ○ s

Full source

theorem subset_comp_self_of_mem_uniformity {s : Set (α × α)} (h : s ∈ 𝓤 α) : s ⊆ s ○ s :=
  subset_comp_self (refl_le_uniformity h)

Self-composition containment for entourages: $s \subseteq s \circ s$ for $s \in \mathfrak{U}(\alpha)$

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, the relation $s$ is contained in its composition with itself, i.e., $s \subseteq s \circ s$.

comp_comp_symm_mem_uniformity_sets theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsSymmetricRel t ∧ t ○ t ○ t ⊆ s

Full source

theorem comp_comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, IsSymmetricRel t ∧ t ○ t ○ t ⊆ s := by
  rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
  rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
  use t, t_in, t_symm
  have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
  -- Porting note: Needed the following `have`s to make `mono` work
  have ht := Subset.refl t
  have hw := Subset.refl w
  calc
    t ○ t ○ t ⊆ w ○ t := by mono
    _ ⊆ w ○ (t ○ t)calc
    t ○ t ○ t ⊆ w ○ t := by mono
    _ ⊆ w ○ (t ○ t) := by mono
    _ ⊆ w ○ wcalc
    t ○ t ○ t ⊆ w ○ t := by mono
    _ ⊆ w ○ (t ○ t) := by mono
    _ ⊆ w ○ w := by mono
    _ ⊆ s := w_sub

Existence of Symmetric Entourage with Triple Composition-Refinement Property

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, there exists a symmetric entourage $t \in \mathfrak{U}(\alpha)$ such that the triple composition $t \circ t \circ t$ is contained in $s$.

UniformSpace.ball definition

(x : β) (V : Set (β × β)) : Set β

Full source

/-- The ball around `(x : β)` with respect to `(V : Set (β × β))`. Intended to be
used for `V ∈ 𝓤 β`, but this is not needed for the definition. Recovers the
notions of metric space ball when `V = {p | dist p.1 p.2 < r }`. -/
def ball (x : β) (V : Set (β × β)) : Set β := Prod.mkProd.mk x ⁻¹' V

Uniform ball centered at a point with respect to an entourage

Informal description

For a uniform space $\beta$, given a point $x \in \beta$ and a set $V \subseteq \beta \times \beta$ (typically an entourage from the uniformity filter $\mathfrak{U} \beta$), the *ball* centered at $x$ with respect to $V$ is defined as the set of all points $y \in \beta$ such that $(x, y) \in V$. This generalizes the notion of a metric ball, where $V$ would be of the form $\{(a, b) \mid d(a, b) < r\}$ for some radius $r > 0$.

UniformSpace.mem_ball_self theorem

(x : α) {V : Set (α × α)} : V ∈ 𝓤 α → x ∈ ball x V

Full source

lemma mem_ball_self (x : α) {V : Set (α × α)} : V ∈ 𝓤 α → x ∈ ball x V := refl_mem_uniformity

Reflexivity of Uniform Balls: $x \in \text{ball}(x, V)$ for all $x$ and entourages $V$

Informal description

For any uniform space $\alpha$, any point $x \in \alpha$, and any entourage $V \in \mathfrak{U}(\alpha)$, the point $x$ belongs to the uniform ball centered at itself with respect to $V$, i.e., $(x, x) \in V$.

UniformSpace.mem_ball_comp theorem

{V W : Set (β × β)} {x y z} (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (V ○ W)

Full source

/-- The triangle inequality for `UniformSpace.ball` -/
theorem mem_ball_comp {V W : Set (β × β)} {x y z} (h : y ∈ ball x V) (h' : z ∈ ball y W) :
    z ∈ ball x (V ○ W) :=
  prodMk_mem_compRel h h'

Triangle Inequality for Uniform Balls: $z \in \text{ball}_x(V \circ W)$ given $y \in \text{ball}_x(V)$ and $z \in \text{ball}_y(W)$

Informal description

For any uniform space $\beta$, entourages $V, W \subseteq \beta \times \beta$, and points $x, y, z \in \beta$, if $y$ is in the uniform ball centered at $x$ with respect to $V$ (i.e., $(x,y) \in V$) and $z$ is in the uniform ball centered at $y$ with respect to $W$ (i.e., $(y,z) \in W$), then $z$ is in the uniform ball centered at $x$ with respect to the composition $V \circ W$ (i.e., $(x,z) \in V \circ W$).

UniformSpace.ball_subset_of_comp_subset theorem

{V W : Set (β × β)} {x y} (h : x ∈ ball y W) (h' : W ○ W ⊆ V) : ball x W ⊆ ball y V

Full source

theorem ball_subset_of_comp_subset {V W : Set (β × β)} {x y} (h : x ∈ ball y W) (h' : W ○ WW ○ W ⊆ V) :
    ballball x W ⊆ ball y V := fun _z z_in => h' (mem_ball_comp h z_in)

Uniform Ball Inclusion via Composition of Entourages: $\text{ball}(x, W) \subseteq \text{ball}(y, V)$ under $x \in \text{ball}(y, W)$ and $W \circ W \subseteq V$

Informal description

Let $\beta$ be a uniform space and $V, W \subseteq \beta \times \beta$ be entourages. For any points $x, y \in \beta$, if $x$ belongs to the uniform ball centered at $y$ with respect to $W$ (i.e., $(y,x) \in W$) and the composition $W \circ W$ is contained in $V$, then the uniform ball centered at $x$ with respect to $W$ is contained in the uniform ball centered at $y$ with respect to $V$.

UniformSpace.ball_mono theorem

{V W : Set (β × β)} (h : V ⊆ W) (x : β) : ball x V ⊆ ball x W

Full source

theorem ball_mono {V W : Set (β × β)} (h : V ⊆ W) (x : β) : ballball x V ⊆ ball x W :=
  preimage_mono h

Monotonicity of Uniform Balls with Respect to Entourage Inclusion

Informal description

For any uniform space $\beta$, if $V$ and $W$ are entourages such that $V \subseteq W$, then for any point $x \in \beta$, the uniform ball centered at $x$ with respect to $V$ is contained in the uniform ball centered at $x$ with respect to $W$.

UniformSpace.ball_inter theorem

(x : β) (V W : Set (β × β)) : ball x (V ∩ W) = ball x V ∩ ball x W

Full source

theorem ball_inter (x : β) (V W : Set (β × β)) : ball x (V ∩ W) = ballball x V ∩ ball x W :=
  preimage_inter

Intersection of Uniform Balls with Respect to Intersection of Entourages

Informal description

For any point $x$ in a uniform space $\beta$ and any two entourages $V, W \subseteq \beta \times \beta$, the ball centered at $x$ with respect to the intersection $V \cap W$ is equal to the intersection of the balls centered at $x$ with respect to $V$ and $W$ respectively. That is: \[ \text{ball}(x, V \cap W) = \text{ball}(x, V) \cap \text{ball}(x, W). \]

UniformSpace.ball_inter_left theorem

(x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x V

Full source

theorem ball_inter_left (x : β) (V W : Set (β × β)) : ballball x (V ∩ W) ⊆ ball x V :=
  ball_mono inter_subset_left x

Left Inclusion of Uniform Balls with Respect to Intersection of Entourages

Informal description

For any point $x$ in a uniform space $\beta$ and any two entourages $V, W \subseteq \beta \times \beta$, the ball centered at $x$ with respect to the intersection $V \cap W$ is contained in the ball centered at $x$ with respect to $V$. That is: \[ \text{ball}(x, V \cap W) \subseteq \text{ball}(x, V). \]

UniformSpace.ball_inter_right theorem

(x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x W

Full source

theorem ball_inter_right (x : β) (V W : Set (β × β)) : ballball x (V ∩ W) ⊆ ball x W :=
  ball_mono inter_subset_right x

Right Inclusion of Uniform Balls with Respect to Entourage Intersection

Informal description

For any point $x$ in a uniform space $\beta$ and any two entourages $V, W \subseteq \beta \times \beta$, the uniform ball centered at $x$ with respect to the intersection $V \cap W$ is contained in the uniform ball centered at $x$ with respect to $W$. That is: \[ \text{ball}(x, V \cap W) \subseteq \text{ball}(x, W). \]

UniformSpace.ball_iInter theorem

{x : β} {V : ι → Set (β × β)} : ball x (⋂ i, V i) = ⋂ i, ball x (V i)

Full source

theorem ball_iInter {x : β} {V : ι → Set (β × β)} : ball x (⋂ i, V i) = ⋂ i, ball x (V i) :=
  preimage_iInter

Intersection of Balls Equals Ball of Intersection in Uniform Spaces

Informal description

For any point $x$ in a uniform space $\beta$ and any family of entourages $\{V_i\}_{i \in \iota}$ in $\beta \times \beta$, the ball centered at $x$ with respect to the intersection $\bigcap_i V_i$ is equal to the intersection of the balls centered at $x$ with respect to each $V_i$: \[ \text{ball}(x, \bigcap_i V_i) = \bigcap_i \text{ball}(x, V_i). \]

UniformSpace.mem_ball_symmetry theorem

{V : Set (β × β)} (hV : IsSymmetricRel V) {x y} : x ∈ ball y V ↔ y ∈ ball x V

Full source

theorem mem_ball_symmetry {V : Set (β × β)} (hV : IsSymmetricRel V) {x y} :
    x ∈ ball y Vx ∈ ball y V ↔ y ∈ ball x V :=
  show (x, y)(x, y) ∈ Prod.swap ⁻¹' V(x, y) ∈ Prod.swap ⁻¹' V ↔ (x, y) ∈ V by
    unfold IsSymmetricRel at hV
    rw [hV]

Symmetry of Uniform Balls for Symmetric Relations

Informal description

For any symmetric relation $ V \subseteq \beta \times \beta $ in a uniform space, and for any points $ x, y \in \beta $, the point $ x $ belongs to the uniform ball centered at $ y $ with respect to $ V $ if and only if $ y $ belongs to the uniform ball centered at $ x $ with respect to $ V $. In other words, $ x \in \text{ball}(y, V) \leftrightarrow y \in \text{ball}(x, V) $.

UniformSpace.ball_eq_of_symmetry theorem

{V : Set (β × β)} (hV : IsSymmetricRel V) {x} : ball x V = {y | (y, x) ∈ V}

Full source

theorem ball_eq_of_symmetry {V : Set (β × β)} (hV : IsSymmetricRel V) {x} :
    ball x V = { y | (y, x) ∈ V } := by
  ext y
  rw [mem_ball_symmetry hV]
  exact Iff.rfl

Characterization of Uniform Balls for Symmetric Relations

Informal description

For any symmetric relation $ V \subseteq \beta \times \beta $ in a uniform space and any point $ x \in \beta $, the uniform ball centered at $ x $ with respect to $ V $ is equal to the set of all points $ y \in \beta $ such that $ (y, x) \in V $. That is, \[ \text{ball}(x, V) = \{ y \in \beta \mid (y, x) \in V \}. \]

UniformSpace.mem_comp_of_mem_ball theorem

 {V W : Set (β × β)} {x y z : β} (hV : IsSymmetricRel V) (hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ V ○ W

Full source

theorem mem_comp_of_mem_ball {V W : Set (β × β)} {x y z : β} (hV : IsSymmetricRel V)
    (hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y)(x, y) ∈ V ○ W := by
  rw [mem_ball_symmetry hV] at hx
  exact ⟨z, hx, hy⟩

Composition of Uniform Balls for Symmetric Relations

Informal description

Let $V$ and $W$ be symmetric relations on a uniform space $\beta$, and let $x, y, z \in \beta$. If $x$ belongs to the uniform ball centered at $z$ with respect to $V$ and $y$ belongs to the uniform ball centered at $z$ with respect to $W$, then the pair $(x, y)$ belongs to the composition $V \circ W$.

UniformSpace.mem_comp_comp theorem

 {V W M : Set (β × β)} (hW' : IsSymmetricRel W) {p : β × β} : p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Full source

theorem mem_comp_comp {V W M : Set (β × β)} (hW' : IsSymmetricRel W) {p : β × β} :
    p ∈ V ○ M ○ Wp ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty := by
  obtain ⟨x, y⟩ := p
  constructor
  · rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
    exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry hW']⟩, hwz⟩
  · rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
    rw [mem_ball_symmetry hW'] at z_in
    exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩

Characterization of Triple Composition in Uniform Spaces via Balls

Informal description

For any symmetric relation $ W \subseteq \beta \times \beta $ in a uniform space, and for any relations $ V, M \subseteq \beta \times \beta $, a pair $ p = (x, y) $ belongs to the composed relation $ V \circ M \circ W $ if and only if the intersection of $ M $ with the Cartesian product of the uniform balls $ \text{ball}(x, V) $ and $ \text{ball}(y, W) $ is nonempty. In other words, $ (x, y) \in V \circ M \circ W $ if and only if there exist points $ a \in \text{ball}(x, V) $ and $ b \in \text{ball}(y, W) $ such that $ (a, b) \in M $.

mem_nhds_uniformity_iff_right theorem

{x : α} {s : Set α} : s ∈ 𝓝 x ↔ {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Full source

theorem mem_nhds_uniformity_iff_right {x : α} {s : Set α} :
    s ∈ 𝓝 xs ∈ 𝓝 x ↔ { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α := by
  simp only [nhds_eq_comap_uniformity, mem_comap_prodMk]

Neighborhood Characterization via Uniformity: Right Version

Informal description

For any point $x$ in a uniform space $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ is a neighborhood of $x$ if and only if the set $\{(p_1, p_2) \in \alpha \times \alpha \mid p_1 = x \implies p_2 \in s\}$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$.

mem_nhds_uniformity_iff_left theorem

{x : α} {s : Set α} : s ∈ 𝓝 x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ 𝓤 α

Full source

theorem mem_nhds_uniformity_iff_left {x : α} {s : Set α} :
    s ∈ 𝓝 xs ∈ 𝓝 x ↔ { p : α × α | p.2 = x → p.1 ∈ s } ∈ 𝓤 α := by
  rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]
  simp only [map_def, mem_map, preimage_setOf_eq, Prod.snd_swap, Prod.fst_swap]

Neighborhood Characterization via Uniformity: Left Version

Informal description

For any point $x$ in a uniform space $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ is a neighborhood of $x$ if and only if the set $\{(p_1, p_2) \in \alpha \times \alpha \mid p_2 = x \implies p_1 \in s\}$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$.

nhdsWithin_eq_comap_uniformity_of_mem theorem

{x : α} {T : Set α} (hx : x ∈ T) (S : Set α) : 𝓝[S] x = (𝓤 α ⊓ 𝓟 (T ×ˢ S)).comap (Prod.mk x)

Full source

theorem nhdsWithin_eq_comap_uniformity_of_mem {x : α} {T : Set α} (hx : x ∈ T) (S : Set α) :
    𝓝[S] x = (𝓤𝓤 α ⊓ 𝓟 (T ×ˢ S)).comap (Prod.mk x) := by
  simp [nhdsWithin, nhds_eq_comap_uniformity, hx]

Neighborhood Filter within Subset as Uniformity Preimage with Domain Restriction

Informal description

For a point $x$ in a uniform space $\alpha$ and subsets $T, S \subseteq \alpha$ with $x \in T$, the neighborhood filter of $x$ within $S$, denoted $\mathcal{N}_S(x)$, is equal to the preimage of the intersection of the uniformity filter $\mathfrak{U}(\alpha)$ with the principal filter of $T \times S$ under the map $y \mapsto (x, y)$. In other words: $$\mathcal{N}_S(x) = \text{comap}_{y \mapsto (x,y)} \left( \mathfrak{U}(\alpha) \cap \mathcal{P}(T \times S) \right)$$

nhdsWithin_eq_comap_uniformity theorem

{x : α} (S : Set α) : 𝓝[S] x = (𝓤 α ⊓ 𝓟 (univ ×ˢ S)).comap (Prod.mk x)

Full source

theorem nhdsWithin_eq_comap_uniformity {x : α} (S : Set α) :
    𝓝[S] x = (𝓤𝓤 α ⊓ 𝓟 (univ ×ˢ S)).comap (Prod.mk x) :=
  nhdsWithin_eq_comap_uniformity_of_mem (mem_univ _) S

Neighborhood Filter within Subset as Uniformity Preimage with Universal Domain

Informal description

For any point $x$ in a uniform space $\alpha$ and any subset $S \subseteq \alpha$, the neighborhood filter of $x$ within $S$, denoted $\mathcal{N}_S(x)$, is equal to the preimage of the intersection of the uniformity filter $\mathfrak{U}(\alpha)$ with the principal filter of $\text{univ} \times S$ under the map $y \mapsto (x, y)$. In other words: $$\mathcal{N}_S(x) = \text{comap}_{y \mapsto (x,y)} \left( \mathfrak{U}(\alpha) \cap \mathcal{P}(\text{univ} \times S) \right)$$

isOpen_iff_ball_subset theorem

{s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s

Full source

/-- See also `isOpen_iff_isOpen_ball_subset`. -/
theorem isOpen_iff_ball_subset {s : Set α} : IsOpenIsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s := by
  simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]

Characterization of Open Sets via Uniform Balls

Informal description

A subset $s$ of a uniform space $\alpha$ is open if and only if for every point $x \in s$, there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that the uniform ball $\text{ball}(x, V) = \{y \in \alpha \mid (x, y) \in V\}$ is entirely contained in $s$.

nhds_basis_uniformity' theorem

 {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x : α} : (𝓝 x).HasBasis p fun i => ball x (s i)

Full source

theorem nhds_basis_uniformity' {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
    {x : α} : (𝓝 x).HasBasis p fun i => ball x (s i) := by
  rw [nhds_eq_comap_uniformity]
  exact h.comap (Prod.mk x)

Neighborhood Basis via Uniformity Basis

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$ having a basis $\{s_i\}_{i \in \iota}$ indexed by a predicate $p$. Then for any point $x \in \alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the uniform balls $\text{ball}(x, s_i)$ for those $i$ where $p(i)$ holds.

nhds_basis_uniformity theorem

 {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x : α} : (𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}

Full source

theorem nhds_basis_uniformity {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
    {x : α} : (𝓝 x).HasBasis p fun i => { y | (y, x) ∈ s i } := by
  replace h := h.comap Prod.swap
  rw [comap_swap_uniformity] at h
  exact nhds_basis_uniformity' h

Neighborhood Basis via Uniformity Basis (Symmetric Form)

Informal description

Let $\alpha$ be a uniform space with a basis $\{s_i\}_{i \in \iota}$ for the uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. Then for any point $x \in \alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the sets $\{y \mid (y, x) \in s_i\}$ for those indices $i$ where $p(i)$ holds.

nhds_eq_comap_uniformity' theorem

{x : α} : 𝓝 x = (𝓤 α).comap fun y => (y, x)

Full source

theorem nhds_eq_comap_uniformity' {x : α} : 𝓝 x = (𝓤 α).comap fun y => (y, x) :=
  (nhds_basis_uniformity (𝓤 α).basis_sets).eq_of_same_basis <| (𝓤 α).basis_sets.comap _

Neighborhood Filter as Uniformity Preimage

Informal description

For any point $x$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ is equal to the preimage of the uniformity filter $\mathfrak{U}(\alpha)$ under the map $y \mapsto (y, x)$.

UniformSpace.mem_nhds_iff theorem

{x : α} {s : Set α} : s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Full source

theorem UniformSpace.mem_nhds_iff {x : α} {s : Set α} : s ∈ 𝓝 xs ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s := by
  rw [nhds_eq_comap_uniformity, mem_comap]
  simp_rw [ball]

Neighborhood Characterization via Uniform Balls

Informal description

For any point $x$ in a uniform space $\alpha$ and any subset $s \subseteq \alpha$, the set $s$ is a neighborhood of $x$ if and only if there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that the uniform ball centered at $x$ with respect to $V$ is contained in $s$.

UniformSpace.ball_mem_nhds theorem

(x : α) ⦃V : Set (α × α)⦄ (V_in : V ∈ 𝓤 α) : ball x V ∈ 𝓝 x

Full source

theorem UniformSpace.ball_mem_nhds (x : α) ⦃V : Set (α × α)⦄ (V_in : V ∈ 𝓤 α) : ballball x V ∈ 𝓝 x := by
  rw [UniformSpace.mem_nhds_iff]
  exact ⟨V, V_in, Subset.rfl⟩

Uniform balls are neighborhoods in uniform spaces

Informal description

For any point $x$ in a uniform space $\alpha$ and any entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$, the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is a neighborhood of $x$.

UniformSpace.ball_mem_nhdsWithin theorem

 {x : α} {S : Set α} ⦃V : Set (α × α)⦄ (x_in : x ∈ S) (V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)) : ball x V ∈ 𝓝[S] x

Full source

theorem UniformSpace.ball_mem_nhdsWithin {x : α} {S : Set α} ⦃V : Set (α × α)⦄ (x_in : x ∈ S)
    (V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)) : ballball x V ∈ 𝓝[S] x := by
  rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]
  exact ⟨V, V_in, Subset.rfl⟩

Uniform Balls as Restricted Neighborhoods in Uniform Spaces

Informal description

For a point $x$ in a uniform space $\alpha$ and a subset $S \subseteq \alpha$ with $x \in S$, if $V$ is an entourage in the uniformity $\mathfrak{U}(\alpha)$ restricted to $S \times S$, then the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is a neighborhood of $x$ within $S$.

UniformSpace.mem_nhds_iff_symm theorem

{x : α} {s : Set α} : s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, IsSymmetricRel V ∧ ball x V ⊆ s

Full source

theorem UniformSpace.mem_nhds_iff_symm {x : α} {s : Set α} :
    s ∈ 𝓝 xs ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, IsSymmetricRel V ∧ ball x V ⊆ s := by
  rw [UniformSpace.mem_nhds_iff]
  constructor
  · rintro ⟨V, V_in, V_sub⟩
    use symmetrizeRel V, symmetrize_mem_uniformity V_in, symmetric_symmetrizeRel V
    exact Subset.trans (ball_mono (symmetrizeRel_subset_self V) x) V_sub
  · rintro ⟨V, V_in, _, V_sub⟩
    exact ⟨V, V_in, V_sub⟩

Neighborhood Characterization via Symmetric Uniform Balls

Informal description

For a uniform space $\alpha$, a subset $s \subseteq \alpha$ is a neighborhood of a point $x \in \alpha$ if and only if there exists a symmetric entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is contained in $s$.

UniformSpace.hasBasis_nhds theorem

(x : α) : HasBasis (𝓝 x) (fun s : Set (α × α) => s ∈ 𝓤 α ∧ IsSymmetricRel s) fun s => ball x s

Full source

theorem UniformSpace.hasBasis_nhds (x : α) :
    HasBasis (𝓝 x) (fun s : Set (α × α) => s ∈ 𝓤 αs ∈ 𝓤 α ∧ IsSymmetricRel s) fun s => ball x s :=
  ⟨fun t => by simp [UniformSpace.mem_nhds_iff_symm, and_assoc]⟩

Neighborhood Basis via Symmetric Entourages in Uniform Spaces

Informal description

For any point $x$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of uniform balls centered at $x$ with respect to symmetric entourages from the uniformity $\mathfrak{U}(\alpha)$. Specifically, for any symmetric entourage $V \in \mathfrak{U}(\alpha)$, the set $\{y \in \alpha \mid (x, y) \in V\}$ forms a neighborhood basis at $x$.

UniformSpace.mem_closure_iff_symm_ball theorem

{s : Set α} {x} : x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → IsSymmetricRel V → (s ∩ ball x V).Nonempty

Full source

theorem UniformSpace.mem_closure_iff_symm_ball {s : Set α} {x} :
    x ∈ closure sx ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → IsSymmetricRel V → (s ∩ ball x V).Nonempty := by
  simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]

Closure Characterization via Symmetric Uniform Balls

Informal description

For any subset $s$ of a uniform space $\alpha$ and any point $x \in \alpha$, $x$ belongs to the closure of $s$ if and only if for every symmetric entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$, the intersection $s \cap \{y \in \alpha \mid (x, y) \in V\}$ is nonempty.

UniformSpace.mem_closure_iff_ball theorem

{s : Set α} {x} : x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty

Full source

theorem UniformSpace.mem_closure_iff_ball {s : Set α} {x} :
    x ∈ closure sx ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty := by
  simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]

Closure Characterization via Uniform Balls

Informal description

For any subset $s$ of a uniform space $\alpha$ and any point $x \in \alpha$, $x$ belongs to the closure of $s$ if and only if for every entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$, the intersection of the uniform ball $\text{ball}(x, V)$ with $s$ is nonempty.

nhds_eq_uniformity theorem

{x : α} : 𝓝 x = (𝓤 α).lift' (ball x)

Full source

theorem nhds_eq_uniformity {x : α} : 𝓝 x = (𝓤 α).lift' (ball x) :=
  (nhds_basis_uniformity' (𝓤 α).basis_sets).eq_biInf

Neighborhood Filter via Uniform Balls

Informal description

For any point $x$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ is equal to the filter generated by the uniform balls $\text{ball}(x, V)$ where $V$ ranges over all entourages in the uniformity filter $\mathfrak{U}(\alpha)$.

nhds_eq_uniformity' theorem

{x : α} : 𝓝 x = (𝓤 α).lift' fun s => {y | (y, x) ∈ s}

Full source

theorem nhds_eq_uniformity' {x : α} : 𝓝 x = (𝓤 α).lift' fun s => { y | (y, x) ∈ s } :=
  (nhds_basis_uniformity (𝓤 α).basis_sets).eq_biInf

Neighborhood Filter via Uniformity (Symmetric Form)

Informal description

For any point $x$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ is equal to the filter generated by the sets $\{y \mid (y, x) \in s\}$ where $s$ ranges over all entourages in the uniformity filter $\mathfrak{U}(\alpha)$.

mem_nhds_left theorem

(x : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : {y : α | (x, y) ∈ s} ∈ 𝓝 x

Full source

theorem mem_nhds_left (x : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : { y : α | (x, y) ∈ s }{ y : α | (x, y) ∈ s } ∈ 𝓝 x :=
  ball_mem_nhds x h

Entourage Neighborhood Property in Uniform Spaces

Informal description

For any point $x$ in a uniform space $\alpha$ and any entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$, the set $\{y \in \alpha \mid (x, y) \in s\}$ is a neighborhood of $x$.

mem_nhds_right theorem

(y : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : {x : α | (x, y) ∈ s} ∈ 𝓝 y

Full source

theorem mem_nhds_right (y : α) {s : Set (α × α)} (h : s ∈ 𝓤 α) : { x : α | (x, y) ∈ s }{ x : α | (x, y) ∈ s } ∈ 𝓝 y :=
  mem_nhds_left _ (symm_le_uniformity h)

Neighborhood Property for Right Entourages in Uniform Spaces

Informal description

For any point $y$ in a uniform space $\alpha$ and any entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$, the set $\{x \in \alpha \mid (x, y) \in s\}$ is a neighborhood of $y$.

exists_mem_nhds_ball_subset_of_mem_nhds theorem

 {a : α} {U : Set α} (h : U ∈ 𝓝 a) : ∃ V ∈ 𝓝 a, ∃ t ∈ 𝓤 α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U

Full source

theorem exists_mem_nhds_ball_subset_of_mem_nhds {a : α} {U : Set α} (h : U ∈ 𝓝 a) :
    ∃ V ∈ 𝓝 a, ∃ t ∈ 𝓤 α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U :=
  let ⟨t, ht, htU⟩ := comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 h)
  ⟨_, mem_nhds_left a ht, t, ht, fun a₁ h₁ a₂ h₂ => @htU (a, a₂) ⟨a₁, h₁, h₂⟩ rfl⟩

Existence of Uniform Neighborhood Refinement

Informal description

For any point $a$ in a uniform space $\alpha$ and any neighborhood $U$ of $a$, there exists a neighborhood $V$ of $a$ and an entourage $t$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $a' \in V$, the uniform ball $\{y \in \alpha \mid (a', y) \in t\}$ is contained in $U$.

tendsto_right_nhds_uniformity theorem

{a : α} : Tendsto (fun a' => (a', a)) (𝓝 a) (𝓤 α)

Full source

theorem tendsto_right_nhds_uniformity {a : α} : Tendsto (fun a' => (a', a)) (𝓝 a) (𝓤 α) := fun _ =>
  mem_nhds_right a

Convergence of Pairs to Uniformity Filter Along Right Projection

Informal description

For any point $a$ in a uniform space $\alpha$, the function $f(a') = (a', a)$ tends to the uniformity filter $\mathfrak{U}(\alpha)$ as $a'$ tends to $a$ in the neighborhood filter $\mathcal{N}(a)$. That is, for any entourage $V \in \mathfrak{U}(\alpha)$, there exists a neighborhood $U \in \mathcal{N}(a)$ such that for all $a' \in U$, the pair $(a', a)$ belongs to $V$.

tendsto_left_nhds_uniformity theorem

{a : α} : Tendsto (fun a' => (a, a')) (𝓝 a) (𝓤 α)

Full source

theorem tendsto_left_nhds_uniformity {a : α} : Tendsto (fun a' => (a, a')) (𝓝 a) (𝓤 α) := fun _ =>
  mem_nhds_left a

Convergence of Pairs to Uniformity Filter Along Left Projection

Informal description

For any point $a$ in a uniform space $\alpha$, the function $f(a') = (a, a')$ tends to the uniformity filter $\mathfrak{U}(\alpha)$ as $a'$ tends to $a$ in the neighborhood filter $\mathcal{N}(a)$. In other words, for any entourage $V \in \mathfrak{U}(\alpha)$, there exists a neighborhood $U \in \mathcal{N}(a)$ such that for all $a' \in U$, the pair $(a, a')$ belongs to $V$.

lift_nhds_left theorem

 {x : α} {g : Set α → Filter β} (hg : Monotone g) : (𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g (ball x s)

Full source

theorem lift_nhds_left {x : α} {g : Set α → Filter β} (hg : Monotone g) :
    (𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g (ball x s) := by
  rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
  simp_rw [ball, Function.comp_def]

Equality of Lifted Neighborhood and Uniformity Filters via Balls

Informal description

Let $\alpha$ be a uniform space and $\beta$ be a type. For any point $x \in \alpha$ and any monotone function $g : \text{Set } \alpha \to \text{Filter } \beta$, the lift of the neighborhood filter $\mathcal{N}(x)$ under $g$ is equal to the lift of the uniformity filter $\mathfrak{U}(\alpha)$ under the function that maps each entourage $s \subseteq \alpha \times \alpha$ to $g(\text{ball}(x, s))$, where $\text{ball}(x, s) = \{y \in \alpha \mid (x, y) \in s\}$.

lift_nhds_right theorem

 {x : α} {g : Set α → Filter β} (hg : Monotone g) : (𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g {y | (y, x) ∈ s}

Full source

theorem lift_nhds_right {x : α} {g : Set α → Filter β} (hg : Monotone g) :
    (𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g { y | (y, x) ∈ s } := by
  rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]
  simp_rw [Function.comp_def, preimage]

Equality of Lifted Neighborhood and Uniformity Filters via Reverse Balls

Informal description

Let $\alpha$ be a uniform space and $\beta$ be a type. For any point $x \in \alpha$ and any monotone function $g : \text{Set } \alpha \to \text{Filter } \beta$, the lift of the neighborhood filter $\mathcal{N}(x)$ under $g$ is equal to the lift of the uniformity filter $\mathfrak{U}(\alpha)$ under the function that maps each entourage $s \subseteq \alpha \times \alpha$ to $g(\{y \in \alpha \mid (y, x) \in s\})$.

nhds_nhds_eq_uniformity_uniformity_prod theorem

 {a b : α} :
  𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s : Set (α × α) => (𝓤 α).lift' fun t => {y : α | (y, a) ∈ s} ×ˢ {y : α | (b, y) ∈ t}

Full source

theorem nhds_nhds_eq_uniformity_uniformity_prod {a b : α} :
    𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s : Set (α × α) =>
      (𝓤 α).lift' fun t => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ t } := by
  rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
  exacts [rfl, monotone_preimage, monotone_preimage]

Product of Neighborhood Filters via Uniformity

Informal description

For any points $a$ and $b$ in a uniform space $\alpha$, the product filter $\mathcal{N}(a) \times \mathcal{N}(b)$ of their neighborhood filters is equal to the filter obtained by lifting the uniformity filter $\mathfrak{U}(\alpha)$ twice: first to construct sets $\{y \mid (y,a) \in s\}$ for entourages $s$, and then to construct sets $\{y \mid (b,y) \in t\}$ for entourages $t$, taking their product. More precisely: \[ \mathcal{N}(a) \times \mathcal{N}(b) = \mathfrak{U}(\alpha).\text{lift} \left( s \mapsto \mathfrak{U}(\alpha).\text{lift}' \left( t \mapsto \{y \mid (y,a) \in s\} \times \{y \mid (b,y) \in t\} \right) \right) \]

Filter.HasBasis.biInter_biUnion_ball theorem

 {p : ι → Prop} {U : ι → Set (α × α)} (h : HasBasis (𝓤 α) p U) (s : Set α) :
  (⋂ (i) (_ : p i), ⋃ x ∈ s, ball x (U i)) = closure s

Full source

theorem Filter.HasBasis.biInter_biUnion_ball {p : ι → Prop} {U : ι → Set (α × α)}
    (h : HasBasis (𝓤 α) p U) (s : Set α) :
    (⋂ (i) (_ : p i), ⋃ x ∈ s, ball x (U i)) = closure s := by
  ext x
  simp [mem_closure_iff_nhds_basis (nhds_basis_uniformity h), ball]

Closure as Intersection of Uniform Neighborhoods

Informal description

Let $\alpha$ be a uniform space with a basis $\{U_i\}_{i \in \iota}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. For any subset $s \subseteq \alpha$, the intersection over all $i$ (where $p(i)$ holds) of the unions $\bigcup_{x \in s} \text{ball}(x, U_i)$ equals the closure of $s$ in $\alpha$. Here, $\text{ball}(x, U_i) = \{y \in \alpha \mid (x, y) \in U_i\}$ denotes the uniform ball centered at $x$ with respect to the entourage $U_i$.

UniformContinuous definition

[UniformSpace β] (f : α → β)

Full source

/-- A function `f : α → β` is *uniformly continuous* if `(f x, f y)` tends to the diagonal
as `(x, y)` tends to the diagonal. In other words, if `x` is sufficiently close to `y`, then
`f x` is close to `f y` no matter where `x` and `y` are located in `α`. -/
def UniformContinuous [UniformSpace β] (f : α → β) :=
  Tendsto (fun x : α × α => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Uniformly continuous function

Informal description

A function $f \colon \alpha \to \beta$ between uniform spaces is *uniformly continuous* if for every entourage $V$ in the uniformity of $\beta$, there exists an entourage $U$ in the uniformity of $\alpha$ such that for all pairs $(x, y) \in U$, the pair $(f(x), f(y))$ belongs to $V$. In other words, $f$ is uniformly continuous if the map $(x, y) \mapsto (f(x), f(y))$ sends entourages in $\alpha$ to entourages in $\beta$.

Uniformity.termUniformContinuous[_,_] definition

: Lean.ParserDescr✝

Full source

/-- Notation for uniform continuity with respect to non-standard `UniformSpace` instances. -/
scoped[Uniformity] notation "UniformContinuous[" u₁ ", " u₂ "]" => @UniformContinuous _ _ u₁ u₂

Notation for uniform continuity with non-standard uniform structures

Informal description

The notation `UniformContinuous[u₁, u₂]` denotes uniform continuity of a function between two uniform spaces with potentially non-standard uniform structures `u₁` (on the domain) and `u₂` (on the codomain).

UniformContinuousOn definition

[UniformSpace β] (f : α → β) (s : Set α) : Prop

Full source

/-- A function `f : α → β` is *uniformly continuous* on `s : Set α` if `(f x, f y)` tends to
the diagonal as `(x, y)` tends to the diagonal while remaining in `s ×ˢ s`.
In other words, if `x` is sufficiently close to `y`, then `f x` is close to
`f y` no matter where `x` and `y` are located in `s`. -/
def UniformContinuousOn [UniformSpace β] (f : α → β) (s : Set α) : Prop :=
  Tendsto (fun x : α × α => (f x.1, f x.2)) (𝓤𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β)

Uniform continuity on a subset

Informal description

A function $ f \colon \alpha \to \beta $ between uniform spaces is *uniformly continuous on a subset $ s \subseteq \alpha $* if for every entourage $ V $ in the uniformity of $ \beta $, there exists an entourage $ U $ in the uniformity of $ \alpha $ such that for all $ (x, y) \in U \cap (s \times s) $, the pair $ (f(x), f(y)) $ belongs to $ V $. This means that $ f $ preserves uniform closeness of points within $ s $.

uniformContinuous_def theorem

 [UniformSpace β] {f : α → β} : UniformContinuous f ↔ ∀ r ∈ 𝓤 β, {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Full source

theorem uniformContinuous_def [UniformSpace β] {f : α → β} :
    UniformContinuousUniformContinuous f ↔ ∀ r ∈ 𝓤 β, { x : α × α | (f x.1, f x.2) ∈ r } ∈ 𝓤 α :=
  Iff.rfl

Characterization of Uniformly Continuous Functions via Uniformities

Informal description

A function $f \colon \alpha \to \beta$ between uniform spaces is uniformly continuous if and only if for every entourage $V$ in the uniformity $\mathfrak{U}(\beta)$ of $\beta$, the preimage $\{(x, y) \in \alpha \times \alpha \mid (f(x), f(y)) \in V\}$ belongs to the uniformity $\mathfrak{U}(\alpha)$ of $\alpha$.

uniformContinuous_iff_eventually theorem

 [UniformSpace β] {f : α → β} : UniformContinuous f ↔ ∀ r ∈ 𝓤 β, ∀ᶠ x : α × α in 𝓤 α, (f x.1, f x.2) ∈ r

Full source

theorem uniformContinuous_iff_eventually [UniformSpace β] {f : α → β} :
    UniformContinuousUniformContinuous f ↔ ∀ r ∈ 𝓤 β, ∀ᶠ x : α × α in 𝓤 α, (f x.1, f x.2) ∈ r :=
  Iff.rfl

Uniform Continuity via Eventual Containment in Uniformities

Informal description

A function $f \colon \alpha \to \beta$ between uniform spaces is uniformly continuous if and only if for every entourage $V$ in the uniformity $\mathfrak{U}(\beta)$ of $\beta$, the set of pairs $(x, y) \in \alpha \times \alpha$ such that $(f(x), f(y)) \in V$ is eventually contained in the uniformity $\mathfrak{U}(\alpha)$ of $\alpha$.

uniformContinuousOn_univ theorem

[UniformSpace β] {f : α → β} : UniformContinuousOn f univ ↔ UniformContinuous f

Full source

theorem uniformContinuousOn_univ [UniformSpace β] {f : α → β} :
    UniformContinuousOnUniformContinuousOn f univ ↔ UniformContinuous f := by
  rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]

Uniform Continuity on Universal Set Equals Global Uniform Continuity

Informal description

A function $f \colon \alpha \to \beta$ between uniform spaces is uniformly continuous on the entire space $\alpha$ if and only if it is uniformly continuous. In other words, uniform continuity on the universal set $\text{univ} = \alpha$ is equivalent to global uniform continuity of $f$.

uniformContinuous_of_const theorem

[UniformSpace β] {c : α → β} (h : ∀ a b, c a = c b) : UniformContinuous c

Full source

theorem uniformContinuous_of_const [UniformSpace β] {c : α → β} (h : ∀ a b, c a = c b) :
    UniformContinuous c :=
  have : (fun x : α × α => (c x.fst, c x.snd)) ⁻¹' idRel = univ :=
    eq_univ_iff_forall.2 fun ⟨a, b⟩ => h a b
  le_trans (map_le_iff_le_comap.2 <| by simp [comap_principal, this, univ_mem]) refl_le_uniformity

Uniform Continuity of Constant Functions

Informal description

For any constant function $c \colon \alpha \to \beta$ between uniform spaces (i.e., a function satisfying $c(a) = c(b)$ for all $a, b \in \alpha$), the function $c$ is uniformly continuous.

uniformContinuous_id theorem

: UniformContinuous (@id α)

Full source

theorem uniformContinuous_id : UniformContinuous (@id α) := tendsto_id

Uniform Continuity of the Identity Function

Informal description

The identity function $\text{id} \colon \alpha \to \alpha$ on a uniform space $\alpha$ is uniformly continuous. That is, for every entourage $V$ in the uniformity of $\alpha$, the pair $(\text{id}(x), \text{id}(y)) = (x, y)$ belongs to $V$ whenever $(x, y)$ is in some entourage $U$ of $\alpha$.

uniformContinuous_const theorem

[UniformSpace β] {b : β} : UniformContinuous fun _ : α => b

Full source

theorem uniformContinuous_const [UniformSpace β] {b : β} : UniformContinuous fun _ : α => b :=
  uniformContinuous_of_const fun _ _ => rfl

Uniform Continuity of Constant Functions

Informal description

For any uniform space $\beta$ and any constant $b \in \beta$, the constant function $f \colon \alpha \to \beta$ defined by $f(x) = b$ for all $x \in \alpha$ is uniformly continuous.

UniformContinuous.comp theorem

 [UniformSpace β] [UniformSpace γ] {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
  UniformContinuous (g ∘ f)

Full source

nonrec theorem UniformContinuous.comp [UniformSpace β] [UniformSpace γ] {g : β → γ} {f : α → β}
    (hg : UniformContinuous g) (hf : UniformContinuous f) : UniformContinuous (g ∘ f) :=
  hg.comp hf

Uniform Continuity is Preserved Under Composition

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces. If $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$ are uniformly continuous functions, then their composition $g \circ f \colon \alpha \to \gamma$ is also uniformly continuous.

UniformContinuous.iterate theorem

[UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) : UniformContinuous T^[n]

Full source

/-- If a function `T` is uniformly continuous in a uniform space `β`,
then its `n`-th iterate `T^[n]` is also uniformly continuous. -/
theorem UniformContinuous.iterate [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) :
    UniformContinuous T^[n] := by
  induction n with
  | zero => exact uniformContinuous_id
  | succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

Uniform Continuity of Iterated Functions

Informal description

Let $T \colon \beta \to \beta$ be a uniformly continuous function on a uniform space $\beta$. Then, for any natural number $n$, the $n$-th iterate $T^{[n]}$ is also uniformly continuous.

Filter.HasBasis.uniformContinuous_iff theorem

 {ι'} [UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop}
  {t : ι' → Set (β × β)} (hb : (𝓤 β).HasBasis q t) {f : α → β} :
  UniformContinuous f ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ t i

Full source

theorem Filter.HasBasis.uniformContinuous_iff {ι'} [UniformSpace β] {p : ι → Prop}
    {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}
    (hb : (𝓤 β).HasBasis q t) {f : α → β} :
    UniformContinuousUniformContinuous f ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ t i :=
  (ha.tendsto_iff hb).trans <| by simp only [Prod.forall]

Uniform Continuity Criterion via Basis Entourages

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with uniformity filters $\mathfrak{U}(\alpha)$ and $\mathfrak{U}(\beta)$ respectively. Suppose $\mathfrak{U}(\alpha)$ has a basis $\{s_j\}_{j \in \iota}$ indexed by $\iota$ with a predicate $p$, and $\mathfrak{U}(\beta)$ has a basis $\{t_i\}_{i \in \iota'}$ indexed by $\iota'$ with a predicate $q$. Then, a function $f \colon \alpha \to \beta$ is uniformly continuous if and only if for every index $i \in \iota'$ satisfying $q(i)$, there exists an index $j \in \iota$ satisfying $p(j)$ such that for all $x, y \in \alpha$, if $(x, y) \in s_j$, then $(f(x), f(y)) \in t_i$.

Filter.HasBasis.uniformContinuousOn_iff theorem

 {ι'} [UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop}
  {t : ι' → Set (β × β)} (hb : (𝓤 β).HasBasis q t) {f : α → β} {S : Set α} :
  UniformContinuousOn f S ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x, x ∈ S → ∀ y, y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i

Full source

theorem Filter.HasBasis.uniformContinuousOn_iff {ι'} [UniformSpace β] {p : ι → Prop}
    {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}
    (hb : (𝓤 β).HasBasis q t) {f : α → β} {S : Set α} :
    UniformContinuousOnUniformContinuousOn f S ↔
      ∀ i, q i → ∃ j, p j ∧ ∀ x, x ∈ S → ∀ y, y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i :=
  ((ha.inf_principal (S ×ˢ S)).tendsto_iff hb).trans <| by
    simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]

Uniform Continuity on Subset Criterion via Basis Entourages

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with uniformity filters $\mathfrak{U}(\alpha)$ and $\mathfrak{U}(\beta)$ having bases $\{s_j\}_{j \in \iota}$ (indexed by $\iota$ with predicate $p$) and $\{t_i\}_{i \in \iota'}$ (indexed by $\iota'$ with predicate $q$) respectively. For a function $f \colon \alpha \to \beta$ and a subset $S \subseteq \alpha$, the following are equivalent: 1. $f$ is uniformly continuous on $S$. 2. For every $i \in \iota'$ with $q(i)$, there exists $j \in \iota$ with $p(j)$ such that for all $x, y \in S$, if $(x, y) \in s_j$ then $(f(x), f(y)) \in t_i$.

Mathlib.Topology.UniformSpace.Defs

Main definitions

Notations

Implementation notes

References