Mathlib.Topology.UniformSpace.Basic

eventually_uniformity_iterate_comp_subset theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) (n : ℕ) : ∀ᶠ t in (𝓤 α).smallSets, (t ○ ·)^[n] t ⊆ s

Full source

/-- If `s ∈ 𝓤 α`, then for any natural `n`, for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ○ ... ○ t ⊆ s` (`n` compositions). -/
theorem eventually_uniformity_iterate_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) (n : ℕ) :
    ∀ᶠ t in (𝓤 α).smallSets, (t ○ ·)^[n] t ⊆ s := by
  suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2
  induction n generalizing s with
  | zero => simpa
  | succ _ ihn =>
    rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
    refine (ihn htU).mono fun U hU => ?_
    rw [Function.iterate_succ_apply']
    exact
      ⟨hU.1.trans <| (subset_comp_self <| refl_le_uniformity htU).trans hts,
        (compRel_mono hU.1 hU.2).trans hts⟩

$n$-fold Composition of Entourages Refines Any Given Entourage

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ and any natural number $n$, there exists a neighborhood $t$ in the filter of small sets of $\mathfrak{U}(\alpha)$ such that the $n$-fold composition $t \circ t \circ \cdots \circ t$ is contained in $s$.

eventually_uniformity_comp_subset theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∀ᶠ t in (𝓤 α).smallSets, t ○ t ⊆ s

Full source

/-- If `s ∈ 𝓤 α`, then for a subset `t` of a sufficiently small set in `𝓤 α`,
we have `t ○ t ⊆ s`. -/
theorem eventually_uniformity_comp_subset {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∀ᶠ t in (𝓤 α).smallSets, t ○ t ⊆ s :=
  eventually_uniformity_iterate_comp_subset hs 1

Composition of Small Entourages Refines Any Given Entourage

Informal description

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

UniformSpace.isOpen_ball theorem

(x : α) {V : Set (α × α)} (hV : IsOpen V) : IsOpen (ball x V)

Full source

lemma isOpen_ball (x : α) {V : Set (α × α)} (hV : IsOpen V) : IsOpen (ball x V) :=
  hV.preimage <| .prodMk_right _

Openness of Uniform Balls with Respect to Open Entourages

Informal description

For any point $x$ in a uniform space $\alpha$ and any open set $V \subseteq \alpha \times \alpha$, the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is an open subset of $\alpha$.

UniformSpace.isClosed_ball theorem

(x : α) {V : Set (α × α)} (hV : IsClosed V) : IsClosed (ball x V)

Full source

lemma isClosed_ball (x : α) {V : Set (α × α)} (hV : IsClosed V) : IsClosed (ball x V) :=
  hV.preimage <| .prodMk_right _

Closedness of Uniform Balls with Respect to Closed Entourages

Informal description

Let $\alpha$ be a uniform space. For any point $x \in \alpha$ and any closed subset $V \subseteq \alpha \times \alpha$, the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is closed in $\alpha$.

UniformSpace.hasBasis_nhds_prod theorem

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

Full source

theorem hasBasis_nhds_prod (x y : α) :
    HasBasis (𝓝 (x, y)) (fun s => s ∈ 𝓤 αs ∈ 𝓤 α ∧ IsSymmetricRel s) fun s => ball x s ×ˢ ball y s := by
  rw [nhds_prod_eq]
  apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)
  rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩
  exact
    ⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, U_symm.inter V_symm⟩, ball_inter_left x U V,
      ball_inter_right y U V⟩

Neighborhood Basis at Product Point via Symmetric Entourages in Uniform Spaces

Informal description

For any two points $x$ and $y$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}((x, y))$ at the point $(x, y)$ has a basis consisting of products of uniform balls centered at $x$ and $y$ with respect to symmetric entourages from the uniformity $\mathfrak{U}(\alpha)$. That is, for any symmetric entourage $s \in \mathfrak{U}(\alpha)$, the set $\text{ball}(x, s) \times \text{ball}(y, s)$ forms a neighborhood basis at $(x, y)$.

nhds_eq_uniformity_prod theorem

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

Full source

theorem nhds_eq_uniformity_prod {a b : α} :
    𝓝 (a, b) =
      (𝓤 α).lift' fun s : Set (α × α) => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ s } := by
  rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
  · exact fun s => monotone_const.set_prod monotone_preimage
  · refine fun t => Monotone.set_prod ?_ monotone_const
    exact monotone_preimage (f := fun y => (y, a))

Neighborhood Filter at Product Point via Uniformity

Informal description

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

nhdset_of_mem_uniformity theorem

 {d : Set (α × α)} (s : Set (α × α)) (hd : d ∈ 𝓤 α) :
  ∃ t : Set (α × α), IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Full source

theorem nhdset_of_mem_uniformity {d : Set (α × α)} (s : Set (α × α)) (hd : d ∈ 𝓤 α) :
    ∃ t : Set (α × α), IsOpen t ∧ s ⊆ t ∧
      t ⊆ { p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d } := by
  let cl_d := { p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d }
  have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
    mem_nhds_iff.mp <|
      show cl_d ∈ 𝓝 (x, y) by
        rw [nhds_eq_uniformity_prod, mem_lift'_sets]
        · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
        · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
  choose t ht using this
  exact ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : Set (α × α)),
    isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left,
    fun ⟨a, b⟩ hp => by
      simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
    iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩

Existence of Open Enlargement via Uniformity Entourage

Informal description

For any entourage $d$ in the uniformity $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ and any set $s \subseteq \alpha \times \alpha$, there exists an open set $t \subseteq \alpha \times \alpha$ such that: 1. $s \subseteq t$, and 2. $t$ is contained in the set $\{(p_1, p_2) \mid \exists x y, (p_1, x) \in d \land (x, y) \in s \land (y, p_2) \in d\}$.

nhds_le_uniformity theorem

(x : α) : 𝓝 (x, x) ≤ 𝓤 α

Full source

/-- Entourages are neighborhoods of the diagonal. -/
theorem nhds_le_uniformity (x : α) : 𝓝 (x, x) ≤ 𝓤 α := by
  intro V V_in
  rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
  have : ballball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
    rw [nhds_prod_eq]
    exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
  apply mem_of_superset this
  rintro ⟨u, v⟩ ⟨u_in, v_in⟩
  exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)

Neighborhood filter at diagonal point refines uniformity

Informal description

For any point $x$ in a uniform space $\alpha$, the neighborhood filter $\mathcal{N}((x, x))$ at the point $(x, x)$ in the product space $\alpha \times \alpha$ is finer than the uniformity filter $\mathfrak{U}(\alpha)$. In other words, every entourage in the uniformity contains a neighborhood of the diagonal point $(x, x)$.

iSup_nhds_le_uniformity theorem

: ⨆ x : α, 𝓝 (x, x) ≤ 𝓤 α

Full source

/-- Entourages are neighborhoods of the diagonal. -/
theorem iSup_nhds_le_uniformity : ⨆ x : α, 𝓝 (x, x) ≤ 𝓤 α :=
  iSup_le nhds_le_uniformity

Supremum of Diagonal Neighborhoods Refines Uniformity

Informal description

For a uniform space $\alpha$, the supremum of the neighborhood filters $\mathcal{N}((x, x))$ over all points $x \in \alpha$ is finer than the uniformity filter $\mathfrak{U}(\alpha)$. In other words, $\bigsqcup_{x \in \alpha} \mathcal{N}((x, x)) \leq \mathfrak{U}(\alpha)$.

nhdsSet_diagonal_le_uniformity theorem

: 𝓝ˢ (diagonal α) ≤ 𝓤 α

Full source

/-- Entourages are neighborhoods of the diagonal. -/
theorem nhdsSet_diagonal_le_uniformity : 𝓝ˢ (diagonal α) ≤ 𝓤 α :=
  (nhdsSet_diagonal α).trans_le iSup_nhds_le_uniformity

Neighborhood Filter of Diagonal Refines Uniformity

Informal description

In a uniform space $\alpha$, the neighborhood filter of the diagonal set $\Delta_\alpha = \{(x,x) \mid x \in \alpha\}$ is finer than the uniformity filter $\mathfrak{U}(\alpha)$. In other words, every entourage in the uniformity contains a neighborhood of the diagonal.

UniformSpace.has_seq_basis theorem

 [IsCountablyGenerated <| 𝓤 α] : ∃ V : ℕ → Set (α × α), HasAntitoneBasis (𝓤 α) V ∧ ∀ n, IsSymmetricRel (V n)

Full source

theorem UniformSpace.has_seq_basis [IsCountablyGenerated <| 𝓤 α] :
    ∃ V : ℕ → Set (α × α), HasAntitoneBasis (𝓤 α) V ∧ ∀ n, IsSymmetricRel (V n) :=
  let ⟨U, hsym, hbasis⟩ := (@UniformSpace.hasBasis_symmetric α _).exists_antitone_subbasis
  ⟨U, hbasis, fun n => (hsym n).2⟩

Existence of Symmetric Antitone Basis for Countably Generated Uniformity

Informal description

For a uniform space $\alpha$ with a countably generated uniformity filter $\mathfrak{U}(\alpha)$, there exists a sequence $(V_n)_{n \in \mathbb{N}}$ of symmetric entourages that forms an antitone basis for $\mathfrak{U}(\alpha)$. That is: 1. The sequence $(V_n)$ is decreasing (antitone). 2. Each $V_n$ is symmetric (i.e., $(x,y) \in V_n$ if and only if $(y,x) \in V_n$). 3. The collection $\{V_n \mid n \in \mathbb{N}\}$ forms a basis for $\mathfrak{U}(\alpha)$.

closure_eq_uniformity theorem

(s : Set <| α × α) : closure s = ⋂ V ∈ {V | V ∈ 𝓤 α ∧ IsSymmetricRel V}, V ○ s ○ V

Full source

theorem closure_eq_uniformity (s : Set <| α × α) :
    closure s = ⋂ V ∈ { V | V ∈ 𝓤 α ∧ IsSymmetricRel V }, V ○ s ○ V := by
  ext ⟨x, y⟩
  simp +contextual only
    [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_setOf_eq,
      and_imp, mem_comp_comp, exists_prop, ← mem_inter_iff, inter_comm, Set.Nonempty]

Closure in Uniform Spaces via Symmetric Entourages

Informal description

For any subset $s$ of $\alpha \times \alpha$ in a uniform space $\alpha$, the closure of $s$ is equal to the intersection over all symmetric entourages $V$ in the uniformity $\mathfrak{U}(\alpha)$ of the composition $V \circ s \circ V$. That is, \[ \overline{s} = \bigcap_{V \in \mathfrak{U}(\alpha), V \text{ symmetric}} V \circ s \circ V. \]

uniformity_hasBasis_closed theorem

: HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsClosed V) id

Full source

theorem uniformity_hasBasis_closed :
    HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 αV ∈ 𝓤 α ∧ IsClosed V) id := by
  refine Filter.hasBasis_self.2 fun t h => ?_
  rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
  refine ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩
  refine Subset.trans ?_ r
  rw [closure_eq_uniformity]
  apply iInter_subset_of_subset
  apply iInter_subset
  exact ⟨w_in, w_symm⟩

Existence of Closed Entourage Basis for Uniformity Filter

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ has a basis consisting of closed entourages. That is, there exists a collection of subsets $V \subseteq \alpha \times \alpha$ such that: 1. Each $V$ belongs to $\mathfrak{U}(\alpha)$ and is closed in the product topology. 2. The collection $\{V \mid V \in \mathfrak{U}(\alpha) \text{ and } V \text{ is closed}\}$ forms a basis for $\mathfrak{U}(\alpha)$.

uniformity_eq_uniformity_closure theorem

: 𝓤 α = (𝓤 α).lift' closure

Full source

theorem uniformity_eq_uniformity_closure : 𝓤 α = (𝓤 α).lift' closure :=
  Eq.symm <| uniformity_hasBasis_closed.lift'_closure_eq_self fun _ => And.right

Uniformity Filter Equals Closure-Lifted Uniformity Filter

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ is equal to the filter generated by the closures of all entourages in $\mathfrak{U}(\alpha)$. That is, \[ \mathfrak{U}(\alpha) = \text{lift}'(\text{closure})(\mathfrak{U}(\alpha)), \] where $\text{lift}'(\text{closure})$ denotes the operation of taking the closure of each entourage in the filter.

Filter.HasBasis.uniformity_closure theorem

 {p : ι → Prop} {U : ι → Set (α × α)} (h : (𝓤 α).HasBasis p U) : (𝓤 α).HasBasis p fun i => closure (U i)

Full source

theorem Filter.HasBasis.uniformity_closure {p : ι → Prop} {U : ι → Set (α × α)}
    (h : (𝓤 α).HasBasis p U) : (𝓤 α).HasBasis p fun i => closure (U i) :=
  (@uniformity_eq_uniformity_closure α _).symm ▸ h.lift'_closure

Uniformity filter basis closure property

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$. Suppose $\mathfrak{U}(\alpha)$ has a basis $\{U_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the collection $\{\overline{U_i}\}_{i \in \iota}$ (where $\overline{U_i}$ denotes the closure of $U_i$) also forms a basis for $\mathfrak{U}(\alpha)$, with the same index set and predicate $p$.

uniformity_hasBasis_closure theorem

: HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α) closure

Full source

/-- Closed entourages form a basis of the uniformity filter. -/
theorem uniformity_hasBasis_closure : HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α) closure :=
  (𝓤 α).basis_sets.uniformity_closure

Uniformity Filter Basis of Closed Entourages

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ has a basis consisting of the closures of all entourages in $\mathfrak{U}(\alpha)$. That is, the collection $\{\overline{V} \mid V \in \mathfrak{U}(\alpha)\}$ forms a basis for $\mathfrak{U}(\alpha)$, where $\overline{V}$ denotes the closure of $V$ in $\alpha \times \alpha$.

closure_eq_inter_uniformity theorem

{t : Set (α × α)} : closure t = ⋂ d ∈ 𝓤 α, d ○ (t ○ d)

Full source

theorem closure_eq_inter_uniformity {t : Set (α × α)} : closure t = ⋂ d ∈ 𝓤 α, d ○ (t ○ d) :=
  calc
    closure t = ⋂ (V) (_ : V ∈ 𝓤 α ∧ IsSymmetricRel V), V ○ t ○ V := closure_eq_uniformity t
    _ = ⋂ V ∈ 𝓤 α, V ○ t ○ V :=
      Eq.symm <|
        UniformSpace.hasBasis_symmetric.biInter_mem fun _ _ hV =>
          compRel_mono (compRel_mono hV Subset.rfl) hV
    _ = ⋂ V ∈ 𝓤 α, V ○ (t ○ V) := by simp only [compRel_assoc]

Closure in Uniform Spaces via Entourage Composition

Informal description

For any subset $t$ of $\alpha \times \alpha$ in a uniform space $\alpha$, the closure of $t$ is equal to the intersection over all entourages $d$ in the uniformity $\mathfrak{U}(\alpha)$ of the composition $d \circ (t \circ d)$. That is, \[ \overline{t} = \bigcap_{d \in \mathfrak{U}(\alpha)} d \circ (t \circ d). \]

uniformity_eq_uniformity_interior theorem

: 𝓤 α = (𝓤 α).lift' interior

Full source

theorem uniformity_eq_uniformity_interior : 𝓤 α = (𝓤 α).lift' interior :=
  le_antisymm
    (le_iInf₂ fun d hd => by
      let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
      let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
      have : s ⊆ interior d :=
        calc
          s ⊆ t := hst
          _ ⊆ interior d :=
            ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
              let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
              hs_comp ⟨x, h₁, y, h₂, h₃⟩
      have : interiorinterior d ∈ 𝓤 α := by filter_upwards [hs] using this
      simp [this])
    fun _ hs => ((𝓤 α).lift' interior).sets_of_superset (mem_lift' hs) interior_subset

Uniformity Filter Equals Interior-Generated Filter

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$ is equal to the filter generated by the interiors of all sets in $\mathfrak{U}(\alpha)$. That is, $\mathfrak{U}(\alpha) = \text{lift}'(\text{interior}, \mathfrak{U}(\alpha))$.

interior_mem_uniformity theorem

{s : Set (α × α)} (hs : s ∈ 𝓤 α) : interior s ∈ 𝓤 α

Full source

theorem interior_mem_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : interiorinterior s ∈ 𝓤 α := by
  rw [uniformity_eq_uniformity_interior]; exact mem_lift' hs

Interior of an Entourage is an Entourage

Informal description

For any entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, the interior of $s$ is also an entourage in $\mathfrak{U}(\alpha)$. That is, if $s \in \mathfrak{U}(\alpha)$, then $\text{interior}(s) \in \mathfrak{U}(\alpha)$.

mem_uniformity_isClosed theorem

{s : Set (α × α)} (h : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsClosed t ∧ t ⊆ s

Full source

theorem mem_uniformity_isClosed {s : Set (α × α)} (h : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsClosed t ∧ t ⊆ s :=
  let ⟨t, ⟨ht_mem, htc⟩, hts⟩ := uniformity_hasBasis_closed.mem_iff.1 h
  ⟨t, ht_mem, htc, hts⟩

Existence of Closed Sub-entourage in Uniformity Filter

Informal description

For any entourage $s$ in the uniformity $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, there exists a closed entourage $t \in \mathfrak{U}(\alpha)$ such that $t \subseteq s$.

isOpen_iff_isOpen_ball_subset theorem

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

Full source

theorem isOpen_iff_isOpen_ball_subset {s : Set α} :
    IsOpenIsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s := by
  rw [isOpen_iff_ball_subset]
  constructor <;> intro h x hx
  · obtain ⟨V, hV, hV'⟩ := h x hx
    exact
      ⟨interior V, interior_mem_uniformity hV, isOpen_interior,
        (ball_mono interior_subset x).trans hV'⟩
  · obtain ⟨V, hV, -, hV'⟩ := h x hx
    exact ⟨V, hV, hV'⟩

Characterization of Open Sets via Open 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 $V$ is open and the uniform ball $\text{ball}(x, V) = \{y \in \alpha \mid (x, y) \in V\}$ is entirely contained in $s$.

Dense.biUnion_uniformity_ball theorem

{s : Set α} {U : Set (α × α)} (hs : Dense s) (hU : U ∈ 𝓤 α) : ⋃ x ∈ s, ball x U = univ

Full source

/-- The uniform neighborhoods of all points of a dense set cover the whole space. -/
theorem Dense.biUnion_uniformity_ball {s : Set α} {U : Set (α × α)} (hs : Dense s) (hU : U ∈ 𝓤 α) :
    ⋃ x ∈ s, ball x U = univ := by
  refine iUnion₂_eq_univ_iff.2 fun y => ?_
  rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y)(x, y) ∈ U⟩
  exact ⟨x, hxs, hxy⟩

Covering Property of Uniform Balls over a Dense Set

Informal description

For a dense subset $s$ of a uniform space $\alpha$ and any entourage $U$ in the uniformity $\mathfrak{U}(\alpha)$, the union of all uniform balls centered at points of $s$ with respect to $U$ covers the entire space $\alpha$, i.e., \[ \bigcup_{x \in s} \{ y \in \alpha \mid (x, y) \in U \} = \alpha. \]

DenseRange.iUnion_uniformity_ball theorem

 {ι : Type*} {xs : ι → α} (xs_dense : DenseRange xs) {U : Set (α × α)} (hU : U ∈ uniformity α) :
  ⋃ i, UniformSpace.ball (xs i) U = univ

Full source

/-- The uniform neighborhoods of all points of a dense indexed collection cover the whole space. -/
lemma DenseRange.iUnion_uniformity_ball {ι : Type*} {xs : ι → α}
    (xs_dense : DenseRange xs) {U : Set (α × α)} (hU : U ∈ uniformity α) :
    ⋃ i, UniformSpace.ball (xs i) U = univ := by
  rw [← biUnion_range (f := xs) (g := fun x ↦ UniformSpace.ball x U)]
  exact Dense.biUnion_uniformity_ball xs_dense hU

Uniform Balls of Dense Range Cover the Space

Informal description

Let $\alpha$ be a uniform space with uniformity $\mathfrak{U}(\alpha)$. Given a dense range of points $\{x_i\}_{i \in \iota}$ in $\alpha$ (i.e., the range of $xs : \iota \to \alpha$ is dense) and any entourage $U \in \mathfrak{U}(\alpha)$, the union of all uniform balls $\bigcup_{i} \{ y \in \alpha \mid (x_i, y) \in U \}$ equals the entire space $\alpha$.

uniformity_hasBasis_open theorem

: HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsOpen V) id

Full source

/-- Open elements of `𝓤 α` form a basis of `𝓤 α`. -/
theorem uniformity_hasBasis_open : HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 αV ∈ 𝓤 α ∧ IsOpen V) id :=
  hasBasis_self.2 fun s hs =>
    ⟨interior s, interior_mem_uniformity hs, isOpen_interior, interior_subset⟩

Open Entourages Form a Basis for the Uniformity Filter

Informal description

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

Filter.HasBasis.mem_uniformity_iff theorem

 {p : β → Prop} {s : β → Set (α × α)} (h : (𝓤 α).HasBasis p s) {t : Set (α × α)} :
  t ∈ 𝓤 α ↔ ∃ i, p i ∧ ∀ a b, (a, b) ∈ s i → (a, b) ∈ t

Full source

theorem Filter.HasBasis.mem_uniformity_iff {p : β → Prop} {s : β → Set (α × α)}
    (h : (𝓤 α).HasBasis p s) {t : Set (α × α)} :
    t ∈ 𝓤 αt ∈ 𝓤 α ↔ ∃ i, p i ∧ ∀ a b, (a, b) ∈ s i → (a, b) ∈ t :=
  h.mem_iff.trans <| by simp only [Prod.forall, subset_def]

Characterization of Uniformity Membership via Basis Elements

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$. Suppose $\mathfrak{U}(\alpha)$ has a basis indexed by $\beta$, where each basis element is characterized by a predicate $p : \beta \to \mathrm{Prop}$ and a family of sets $s : \beta \to \mathrm{Set}(\alpha \times \alpha)$. Then, for any set $t \subseteq \alpha \times \alpha$, we have $t \in \mathfrak{U}(\alpha)$ if and only if there exists an index $i \in \beta$ such that $p(i)$ holds and for all $a, b \in \alpha$, if $(a, b) \in s(i)$ then $(a, b) \in t$.

uniformity_hasBasis_open_symmetric theorem

: HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 α ∧ IsOpen V ∧ IsSymmetricRel V) id

Full source

/-- Open elements `s : Set (α × α)` of `𝓤 α` such that `(x, y) ∈ s ↔ (y, x) ∈ s` form a basis
of `𝓤 α`. -/
theorem uniformity_hasBasis_open_symmetric :
    HasBasis (𝓤 α) (fun V : Set (α × α) => V ∈ 𝓤 αV ∈ 𝓤 α ∧ IsOpen V ∧ IsSymmetricRel V) id := by
  simp only [← and_assoc]
  refine uniformity_hasBasis_open.restrict fun s hs => ⟨symmetrizeRel s, ?_⟩
  exact
    ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
      symmetric_symmetrizeRel s, symmetrizeRel_subset_self s⟩

Open Symmetric Entourages Form a Basis for the Uniformity Filter

Informal description

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

comp_open_symm_mem_uniformity_sets theorem

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

Full source

theorem comp_open_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, IsOpen t ∧ IsSymmetricRel t ∧ t ○ t ⊆ s := by
  obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
  obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁
  exact ⟨u, hu₁, hu₂, hu₃, (compRel_mono hu₄ hu₄).trans ht₂⟩

Existence of Open Symmetric Entourage with Composition Property in Uniformity Filter

Informal description

For any entourage $s$ in the uniformity filter $\mathfrak{U}(\alpha)$ of a uniform space $\alpha$, there exists an entourage $t \in \mathfrak{U}(\alpha)$ that is open, symmetric, and satisfies the composition property $t \circ t \subseteq s$.

instPartialOrderUniformSpace instance

: PartialOrder (UniformSpace α)

Full source

instance : PartialOrder (UniformSpace α) :=
  PartialOrder.lift (fun u => 𝓤[u]) fun _ _ => UniformSpace.ext

Partial Order on Uniform Space Structures

Informal description

The collection of uniform space structures on a type $\alpha$ forms a partial order, where one uniform structure is less than or equal to another if its uniformity filter is finer (i.e., contains more entourages).

UniformSpace.le_def theorem

{u₁ u₂ : UniformSpace α} : u₁ ≤ u₂ ↔ 𝓤[u₁] ≤ 𝓤[u₂]

Full source

protected theorem UniformSpace.le_def {u₁ u₂ : UniformSpace α} : u₁ ≤ u₂ ↔ 𝓤[u₁] ≤ 𝓤[u₂] := Iff.rfl

Uniform Space Order Criterion via Uniformity Filters

Informal description

For two uniform space structures $u_1$ and $u_2$ on a type $\alpha$, the statement $u_1 \leq u_2$ holds if and only if the uniformity filter $\mathfrak{U}(u_1)$ is finer than $\mathfrak{U}(u_2)$, meaning that every entourage in $\mathfrak{U}(u_2)$ is also an entourage in $\mathfrak{U}(u_1)$.

instInfSetUniformSpace instance

: InfSet (UniformSpace α)

Full source

instance : InfSet (UniformSpace α) :=
  ⟨fun s =>
    UniformSpace.ofCore
      { uniformity := ⨅ u ∈ s, 𝓤[u]
        refl := le_iInf fun u => le_iInf fun _ => u.toCore.refl
        symm := le_iInf₂ fun u hu =>
          le_trans (map_mono <| iInf_le_of_le _ <| iInf_le _ hu) u.symm
        comp := le_iInf₂ fun u hu =>
          le_trans (lift'_mono (iInf_le_of_le _ <| iInf_le _ hu) <| le_rfl) u.comp }⟩

Complete Lattice Structure on Uniform Spaces

Informal description

The collection of uniform space structures on a type $\alpha$ forms a complete lattice, where the infimum of a set of uniform structures is given by the intersection of their uniformity filters.

UniformSpace.sInf_le theorem

{tt : Set (UniformSpace α)} {t : UniformSpace α} (h : t ∈ tt) : sInf tt ≤ t

Full source

protected theorem UniformSpace.sInf_le {tt : Set (UniformSpace α)} {t : UniformSpace α}
    (h : t ∈ tt) : sInf tt ≤ t :=
  show ⨅ u ∈ tt, 𝓤[u] ≤ 𝓤[t] from iInf₂_le t h

Infimum of Uniform Space Structures is Finer than Each Member

Informal description

For any collection of uniform space structures $\mathcal{tt}$ on a type $\alpha$ and any uniform space structure $t \in \mathcal{tt}$, the infimum of $\mathcal{tt}$ is finer than or equal to $t$. In other words, the uniformity filter of $\bigsqcap \mathcal{tt}$ is contained in the uniformity filter of $t$.

UniformSpace.le_sInf theorem

{tt : Set (UniformSpace α)} {t : UniformSpace α} (h : ∀ t' ∈ tt, t ≤ t') : t ≤ sInf tt

Full source

protected theorem UniformSpace.le_sInf {tt : Set (UniformSpace α)} {t : UniformSpace α}
    (h : ∀ t' ∈ tt, t ≤ t') : t ≤ sInf tt :=
  show 𝓤[t] ≤ ⨅ u ∈ tt, 𝓤[u] from le_iInf₂ h

Infimum of Uniform Space Structures is Greatest Lower Bound

Informal description

Let $\alpha$ be a type, and let $\mathcal{tt}$ be a set of uniform space structures on $\alpha$. For any uniform space structure $t$ on $\alpha$, if $t$ is less than or equal to every uniform space structure $t' \in \mathcal{tt}$, then $t$ is less than or equal to the infimum of $\mathcal{tt}$. In other words, the infimum of a set of uniform space structures is the greatest lower bound with respect to the partial order on uniform space structures.

instTopUniformSpace instance

: Top (UniformSpace α)

Full source

instance : Top (UniformSpace α) :=
  ⟨@UniformSpace.mk α ⊤ ⊤ le_top le_top fun x ↦ by simp only [nhds_top, comap_top]⟩

The Greatest Uniform Space Structure on a Type

Informal description

For any type $\alpha$, the collection of uniform space structures on $\alpha$ has a greatest element with respect to the partial order of uniform space structures. This greatest uniform space structure is the one where the uniformity filter is the coarsest possible, containing all subsets of $\alpha \times \alpha$ that include the diagonal.

instBotUniformSpace instance

: Bot (UniformSpace α)

Full source

instance : Bot (UniformSpace α) :=
  ⟨{  toTopologicalSpace := ⊥
      uniformity := 𝓟 idRel
      symm := by simp [Tendsto]
      comp := lift'_le (mem_principal_self _) <| principal_mono.2 id_compRel.subset
      nhds_eq_comap_uniformity := fun s => by
        let _ : TopologicalSpace α := ⊥; have := discreteTopology_bot α
        simp [idRel] }⟩

The Trivial Uniform Space Structure

Informal description

For any type $\alpha$, the trivial uniform space structure on $\alpha$ is the smallest element in the complete lattice of uniform space structures on $\alpha$. This structure has the coarsest uniformity, where the only entourages are those containing the diagonal relation.

instMinUniformSpace instance

: Min (UniformSpace α)

Full source

instance : Min (UniformSpace α) :=
  ⟨fun u₁ u₂ =>
    { uniformity := 𝓤[u₁] ⊓ 𝓤[u₂]
      symm := u₁.symm.inf u₂.symm
      comp := (lift'_inf_le _ _ _).trans <| inf_le_inf u₁.comp u₂.comp
      toTopologicalSpace := u₁.toTopologicalSpace ⊓ u₂.toTopologicalSpace
      nhds_eq_comap_uniformity := fun _ ↦ by
        rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf] }⟩

Meet-Semilattice Structure on Uniform Spaces

Informal description

The collection of uniform space structures on a type $\alpha$ forms a meet-semilattice, where the minimum operation is given by the intersection of uniformities.

instCompleteLatticeUniformSpace instance

: CompleteLattice (UniformSpace α)

Full source

instance : CompleteLattice (UniformSpace α) :=
  { inferInstanceAs (PartialOrder (UniformSpace α)) with
    sup := fun a b => sInf { x | a ≤ x ∧ b ≤ x }
    le_sup_left := fun _ _ => UniformSpace.le_sInf fun _ ⟨h, _⟩ => h
    le_sup_right := fun _ _ => UniformSpace.le_sInf fun _ ⟨_, h⟩ => h
    sup_le := fun _ _ _ h₁ h₂ => UniformSpace.sInf_le ⟨h₁, h₂⟩
    inf := (· ⊓ ·)
    le_inf := fun a _ _ h₁ h₂ => show a.uniformity ≤ _ from le_inf h₁ h₂
    inf_le_left := fun a _ => show _ ≤ a.uniformity from inf_le_left
    inf_le_right := fun _ b => show _ ≤ b.uniformity from inf_le_right
    top := ⊤
    le_top := fun a => show a.uniformity ≤ ⊤ from le_top
    bot := ⊥
    bot_le := fun u => u.toCore.refl
    sSup := fun tt => sInf { t | ∀ t' ∈ tt, t' ≤ t }
    le_sSup := fun _ _ h => UniformSpace.le_sInf fun _ h' => h' _ h
    sSup_le := fun _ _ h => UniformSpace.sInf_le h
    sInf := sInf
    le_sInf := fun _ _ hs => UniformSpace.le_sInf hs
    sInf_le := fun _ _ ha => UniformSpace.sInf_le ha }

Complete Lattice Structure on Uniform Spaces

Informal description

The collection of uniform space structures on a type $\alpha$ forms a complete lattice, where the partial order is given by the fineness of the uniformity filters, and meets and joins are constructed via intersections and unions of these filters respectively.

iInf_uniformity theorem

{ι : Sort*} {u : ι → UniformSpace α} : 𝓤[iInf u] = ⨅ i, 𝓤[u i]

Full source

theorem iInf_uniformity {ι : Sort*} {u : ι → UniformSpace α} : 𝓤[iInf u] = ⨅ i, 𝓤[u i] :=
  iInf_range

Uniformity Filter of Infimum of Uniform Spaces Equals Infimum of Uniformity Filters

Informal description

For any indexed family of uniform space structures $(u_i)_{i \in \iota}$ on a type $\alpha$, the uniformity filter of the infimum uniform space $\bigsqcap_i u_i$ is equal to the infimum of the uniformity filters $\bigsqcap_i \mathfrak{U}(u_i)$. That is, \[ \mathfrak{U}\left(\bigsqcap_{i \in \iota} u_i\right) = \bigsqcap_{i \in \iota} \mathfrak{U}(u_i). \]

inf_uniformity theorem

{u v : UniformSpace α} : 𝓤[u ⊓ v] = 𝓤[u] ⊓ 𝓤[v]

Full source

theorem inf_uniformity {u v : UniformSpace α} : 𝓤[u ⊓ v] = 𝓤[u]𝓤[u] ⊓ 𝓤[v] := rfl

Uniformity of Infimum of Uniform Spaces

Informal description

For any two uniform space structures $u$ and $v$ on a type $\alpha$, the uniformity of their infimum $u \sqcap v$ is equal to the infimum of their uniformities, i.e., $\mathfrak{U}(u \sqcap v) = \mathfrak{U}(u) \sqcap \mathfrak{U}(v)$.

bot_uniformity theorem

: 𝓤[(⊥ : UniformSpace α)] = 𝓟 idRel

Full source

lemma bot_uniformity : 𝓤[(⊥ : UniformSpace α)] = 𝓟 idRel := rfl

Uniformity of Trivial Uniform Space Equals Principal Filter of Identity Relation

Informal description

For the trivial uniform space structure $\bot$ on a type $\alpha$, the uniformity filter $\mathfrak{U}(\bot)$ is equal to the principal filter generated by the identity relation $\{(x, x) \mid x \in \alpha\}$.

top_uniformity theorem

: 𝓤[(⊤ : UniformSpace α)] = ⊤

Full source

lemma top_uniformity : 𝓤[(⊤ : UniformSpace α)] = ⊤ := rfl

Uniformity of the Greatest Uniform Space is Trivial

Informal description

The uniformity filter of the greatest uniform space structure on a type $\alpha$ is the trivial filter $\top$ (the filter containing all subsets of $\alpha \times \alpha$).

inhabitedUniformSpace instance

: Inhabited (UniformSpace α)

Full source

instance inhabitedUniformSpace : Inhabited (UniformSpace α) :=
  ⟨⊥⟩

Nonempty Uniform Space Structures

Informal description

For any type $\alpha$, the collection of uniform space structures on $\alpha$ is nonempty.

inhabitedUniformSpaceCore instance

: Inhabited (UniformSpace.Core α)

Full source

instance inhabitedUniformSpaceCore : Inhabited (UniformSpace.Core α) :=
  ⟨@UniformSpace.toCore _ default⟩

Nonempty Uniform Space Cores

Informal description

For any type $\alpha$, the collection of uniform space cores on $\alpha$ is nonempty.

instUniqueUniformSpaceOfSubsingleton instance

[Subsingleton α] : Unique (UniformSpace α)

Full source

instance [Subsingleton α] : Unique (UniformSpace α) where
  uniq u := bot_unique <| le_principal_iff.2 <| by
    rw [idRel, ← diagonal, diagonal_eq_univ]; exact univ_mem

Unique Uniform Space Structure on Subsingleton Types

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton), there is a unique uniform space structure on $\alpha$.

UniformSpace.comap abbrev

(f : α → β) (u : UniformSpace β) : UniformSpace α

Full source

/-- Given `f : α → β` and a uniformity `u` on `β`, the inverse image of `u` under `f`
  is the inverse image in the filter sense of the induced function `α × α → β × β`.
  See note [reducible non-instances]. -/
abbrev UniformSpace.comap (f : α → β) (u : UniformSpace β) : UniformSpace α where
  uniformity := 𝓤[u].comap fun p : α × α => (f p.1, f p.2)
  symm := by
    simp only [tendsto_comap_iff, Prod.swap, (· ∘ ·)]
    exact tendsto_swap_uniformity.comp tendsto_comap
  comp := le_trans
    (by
      rw [comap_lift'_eq, comap_lift'_eq2]
      · exact lift'_mono' fun s _ ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩ => ⟨f x, h₁, h₂⟩
      · exact monotone_id.compRel monotone_id)
    (comap_mono u.comp)
  toTopologicalSpace := u.toTopologicalSpace.induced f
  nhds_eq_comap_uniformity x := by
    simp only [nhds_induced, nhds_eq_comap_uniformity, comap_comap, Function.comp_def]

Pullback Uniform Space Structure via Function

Informal description

Given a function $f \colon \alpha \to \beta$ and a uniform space structure on $\beta$, the pullback uniform space structure on $\alpha$ is defined such that its uniformity filter is the preimage of the uniformity filter on $\beta$ under the map $(f \times f) \colon \alpha \times \alpha \to \beta \times \beta$.

uniformity_comap theorem

{_ : UniformSpace β} (f : α → β) : 𝓤[UniformSpace.comap f ‹_›] = comap (Prod.map f f) (𝓤 β)

Full source

theorem uniformity_comap {_ : UniformSpace β} (f : α → β) :
    𝓤[UniformSpace.comap f ‹_›] = comap (Prod.map f f) (𝓤 β) :=
  rfl

Uniformity Filter of Pullback Uniform Space via Preimage

Informal description

For any function $f \colon \alpha \to \beta$ between uniform spaces, the uniformity filter $\mathfrak{U}(\alpha)$ induced by the pullback uniform space structure on $\alpha$ is equal to the preimage of the uniformity filter $\mathfrak{U}(\beta)$ under the product map $f \times f \colon \alpha \times \alpha \to \beta \times \beta$. In symbols: \[ \mathfrak{U}_{\text{comap } f} = (f \times f)^{-1}(\mathfrak{U}_\beta). \]

ball_preimage theorem

 {f : α → β} {U : Set (β × β)} {x : α} : UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

Full source

lemma ball_preimage {f : α → β} {U : Set (β × β)} {x : α} :
    UniformSpace.ball x (Prod.mapProd.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U := by
  ext : 1
  simp only [UniformSpace.ball, mem_preimage, Prod.map_apply]

Preimage of Uniform Ball Equals Ball of Preimage

Informal description

For any function $f \colon \alpha \to \beta$ between uniform spaces, any entourage $U \subseteq \beta \times \beta$, and any point $x \in \alpha$, the preimage of the uniform ball centered at $f(x)$ with respect to $U$ under $f$ is equal to the uniform ball centered at $x$ with respect to the preimage of $U$ under the product map $f \times f$. That is, \[ f^{-1}\big(\text{ball}(f(x), U)\big) = \text{ball}\big(x, (f \times f)^{-1}(U)\big). \]

uniformSpace_comap_id theorem

{α : Type*} : UniformSpace.comap (id : α → α) = id

Full source

@[simp]
theorem uniformSpace_comap_id {α : Type*} : UniformSpace.comap (id : α → α) = id := by
  ext : 2
  rw [uniformity_comap, Prod.map_id, comap_id]

Identity Function Preserves Uniform Space Structure via Pullback

Informal description

For any type $\alpha$, the pullback uniform space structure induced by the identity function $\text{id} \colon \alpha \to \alpha$ is equal to the identity function on uniform space structures. That is, $\text{UniformSpace.comap}(\text{id}) = \text{id}$.

UniformSpace.comap_comap theorem

 {α β γ} {uγ : UniformSpace γ} {f : α → β} {g : β → γ} :
  UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ)

Full source

theorem UniformSpace.comap_comap {α β γ} {uγ : UniformSpace γ} {f : α → β} {g : β → γ} :
    UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ) := by
  ext1
  simp only [uniformity_comap, Filter.comap_comap, Prod.map_comp_map]

Composition Law for Pullback Uniform Structures

Informal description

For any uniform space $\gamma$ and functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the pullback uniform structure on $\alpha$ obtained via the composition $g \circ f$ is equal to the pullback uniform structure on $\alpha$ obtained by first pulling back along $g$ to $\beta$ and then pulling back along $f$ to $\alpha$. In other words, the following equality holds: \[ \text{UniformSpace.comap}(g \circ f, u_\gamma) = \text{UniformSpace.comap}(f, \text{UniformSpace.comap}(g, u_\gamma)). \]

UniformSpace.comap_inf theorem

{α γ} {u₁ u₂ : UniformSpace γ} {f : α → γ} : (u₁ ⊓ u₂).comap f = u₁.comap f ⊓ u₂.comap f

Full source

theorem UniformSpace.comap_inf {α γ} {u₁ u₂ : UniformSpace γ} {f : α → γ} :
    (u₁ ⊓ u₂).comap f = u₁.comap f ⊓ u₂.comap f :=
  UniformSpace.ext Filter.comap_inf

Pullback of Infimum of Uniform Structures Equals Infimum of Pullbacks

Informal description

For any type $\alpha$ and $\gamma$, given two uniform space structures $u_1$ and $u_2$ on $\gamma$ and a function $f \colon \alpha \to \gamma$, the pullback of the infimum of $u_1$ and $u_2$ along $f$ is equal to the infimum of the pullbacks of $u_1$ and $u_2$ along $f$. In other words: $$(u_1 \sqcap u_2).\text{comap}\, f = u_1.\text{comap}\, f \sqcap u_2.\text{comap}\, f$$

UniformSpace.comap_iInf theorem

{ι α γ} {u : ι → UniformSpace γ} {f : α → γ} : (⨅ i, u i).comap f = ⨅ i, (u i).comap f

Full source

theorem UniformSpace.comap_iInf {ι α γ} {u : ι → UniformSpace γ} {f : α → γ} :
    (⨅ i, u i).comap f = ⨅ i, (u i).comap f := by
  ext : 1
  simp [uniformity_comap, iInf_uniformity]

Pullback of Infimum Uniform Structure Equals Infimum of Pullbacks

Informal description

For any indexed family of uniform space structures $(u_i)_{i \in \iota}$ on a type $\gamma$ and any function $f \colon \alpha \to \gamma$, the pullback of the infimum uniform structure $\bigsqcap_i u_i$ along $f$ is equal to the infimum of the pullbacks of each $u_i$ along $f$. That is, \[ \left(\bigsqcap_{i \in \iota} u_i\right).\mathrm{comap}\, f = \bigsqcap_{i \in \iota} (u_i.\mathrm{comap}\, f). \]

UniformSpace.comap_mono theorem

{α γ} {f : α → γ} : Monotone fun u : UniformSpace γ => u.comap f

Full source

theorem UniformSpace.comap_mono {α γ} {f : α → γ} :
    Monotone fun u : UniformSpace γ => u.comap f := fun _ _ hu =>
  Filter.comap_mono hu

Monotonicity of Uniform Space Pullback Operation

Informal description

For any function $f \colon \alpha \to \gamma$, the pullback operation $\text{comap}\, f$ on uniform space structures is monotone. That is, if $u_1$ and $u_2$ are uniform space structures on $\gamma$ with $u_1 \leq u_2$, then $u_1.\text{comap}\, f \leq u_2.\text{comap}\, f$ as uniform space structures on $\alpha$.

uniformContinuous_iff theorem

{α β} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} : UniformContinuous f ↔ uα ≤ uβ.comap f

Full source

theorem uniformContinuous_iff {α β} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} :
    UniformContinuousUniformContinuous f ↔ uα ≤ uβ.comap f :=
  Filter.map_le_iff_le_comap

Uniform Continuity Criterion via Pullback Uniformity

Informal description

A function $f \colon \alpha \to \beta$ between uniform spaces is uniformly continuous if and only if the uniform structure on $\alpha$ is finer than the pullback of the uniform structure on $\beta$ via $f$. In other words, $f$ is uniformly continuous precisely when the uniformity filter on $\alpha$ contains all preimages of entourages from $\beta$ under the map $(f \times f) \colon \alpha \times \alpha \to \beta \times \beta$.

le_iff_uniformContinuous_id theorem

{u v : UniformSpace α} : u ≤ v ↔ @UniformContinuous _ _ u v id

Full source

theorem le_iff_uniformContinuous_id {u v : UniformSpace α} :
    u ≤ v ↔ @UniformContinuous _ _ u v id := by
  rw [uniformContinuous_iff, uniformSpace_comap_id, id]

Uniform Structure Comparison via Identity Function's Uniform Continuity

Informal description

For any two uniform space structures $u$ and $v$ on a type $\alpha$, the structure $u$ is finer than $v$ (i.e., $u \leq v$) if and only if the identity function $\text{id} \colon (\alpha, u) \to (\alpha, v)$ is uniformly continuous.

uniformContinuous_comap theorem

{f : α → β} [u : UniformSpace β] : @UniformContinuous α β (UniformSpace.comap f u) u f

Full source

theorem uniformContinuous_comap {f : α → β} [u : UniformSpace β] :
    @UniformContinuous α β (UniformSpace.comap f u) u f :=
  tendsto_comap

Uniform Continuity of Pullback Uniform Structure

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces, where $\beta$ is equipped with a uniform space structure. Then $f$ is uniformly continuous when $\alpha$ is equipped with the pullback uniform structure induced by $f$.

uniformContinuous_comap' theorem

 {f : γ → β} {g : α → γ} [v : UniformSpace β] [u : UniformSpace α] (h : UniformContinuous (f ∘ g)) :
  @UniformContinuous α γ u (UniformSpace.comap f v) g

Full source

theorem uniformContinuous_comap' {f : γ → β} {g : α → γ} [v : UniformSpace β] [u : UniformSpace α]
    (h : UniformContinuous (f ∘ g)) : @UniformContinuous α γ u (UniformSpace.comap f v) g :=
  tendsto_comap_iff.2 h

Uniform Continuity of Function under Pullback Uniform Structure

Informal description

Let $f \colon \gamma \to \beta$ and $g \colon \alpha \to \gamma$ be functions between uniform spaces, with $\beta$ equipped with a uniform structure $v$ and $\alpha$ with a uniform structure $u$. If the composition $f \circ g$ is uniformly continuous, then $g$ is uniformly continuous when $\gamma$ is equipped with the pullback uniform structure induced by $f$ from $v$.

UniformSpace.to_nhds_mono theorem

 {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) (a : α) :
  @nhds _ (@UniformSpace.toTopologicalSpace _ u₁) a ≤ @nhds _ (@UniformSpace.toTopologicalSpace _ u₂) a

Full source

theorem to_nhds_mono {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) (a : α) :
    @nhds _ (@UniformSpace.toTopologicalSpace _ u₁) a ≤
      @nhds _ (@UniformSpace.toTopologicalSpace _ u₂) a := by
  rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]; exact lift'_mono h le_rfl

Monotonicity of Neighborhood Filters with Respect to Uniform Space Ordering

Informal description

Let $u_1$ and $u_2$ be two uniform space structures on a type $\alpha$ such that $u_1 \leq u_2$ (i.e., the uniformity of $u_1$ is finer than that of $u_2$). Then, for any point $a \in \alpha$, the neighborhood filter at $a$ induced by the topology of $u_1$ is finer than the neighborhood filter at $a$ induced by the topology of $u_2$.

UniformSpace.toTopologicalSpace_mono theorem

 {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) : @UniformSpace.toTopologicalSpace _ u₁ ≤ @UniformSpace.toTopologicalSpace _ u₂

Full source

theorem toTopologicalSpace_mono {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) :
    @UniformSpace.toTopologicalSpace _ u₁ ≤ @UniformSpace.toTopologicalSpace _ u₂ :=
  le_of_nhds_le_nhds <| to_nhds_mono h

Monotonicity of Induced Topology with Respect to Uniform Space Ordering

Informal description

Let $u_1$ and $u_2$ be two uniform space structures on a type $\alpha$ such that $u_1 \leq u_2$ (i.e., the uniformity of $u_1$ is finer than that of $u_2$). Then the topology induced by $u_1$ is finer than the topology induced by $u_2$.

UniformSpace.toTopologicalSpace_comap theorem

 {f : α → β} {u : UniformSpace β} :
  @UniformSpace.toTopologicalSpace _ (UniformSpace.comap f u) =
    TopologicalSpace.induced f (@UniformSpace.toTopologicalSpace β u)

Full source

theorem toTopologicalSpace_comap {f : α → β} {u : UniformSpace β} :
    @UniformSpace.toTopologicalSpace _ (UniformSpace.comap f u) =
      TopologicalSpace.induced f (@UniformSpace.toTopologicalSpace β u) :=
  rfl

Compatibility of Pullback Uniform Space Topology with Induced Topology

Informal description

For any function $f \colon \alpha \to \beta$ and uniform space structure $u$ on $\beta$, the topology induced by the pullback uniform space structure $\text{UniformSpace.comap}\,f\,u$ on $\alpha$ coincides with the topology obtained by pulling back the topology of $\beta$ via $f$. In other words, the following equality holds between topological spaces: \[ \text{UniformSpace.toTopologicalSpace}\,(\text{UniformSpace.comap}\,f\,u) = \text{TopologicalSpace.induced}\,f\,(\text{UniformSpace.toTopologicalSpace}\,\beta\,u). \]

UniformSpace.uniformSpace_eq_bot theorem

{u : UniformSpace α} : u = ⊥ ↔ idRel ∈ 𝓤[u]

Full source

lemma uniformSpace_eq_bot {u : UniformSpace α} : u = ⊥ ↔ idRel ∈ 𝓤[u] :=
  le_bot_iff.symm.trans le_principal_iff

Characterization of Trivial Uniform Space via Identity Relation

Informal description

For a uniform space structure $u$ on a type $\alpha$, the structure $u$ is the trivial uniform space (i.e., $u = \bot$) if and only if the identity relation $\{(x, x) \mid x \in \alpha\}$ is an entourage in the uniformity $\mathfrak{U}[u]$.

Filter.HasBasis.uniformSpace_eq_bot theorem

 {ι p} {s : ι → Set (α × α)} {u : UniformSpace α} (h : 𝓤[u].HasBasis p s) :
  u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y : α ↦ (x, y) ∉ s i

Full source

protected lemma _root_.Filter.HasBasis.uniformSpace_eq_bot {ι p} {s : ι → Set (α × α)}
    {u : UniformSpace α} (h : 𝓤[u].HasBasis p s) :
    u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y : α ↦ (x, y) ∉ s i := by
  simp [uniformSpace_eq_bot, h.mem_iff, subset_def, Pairwise, not_imp_not]

Characterization of Trivial Uniform Space via Basis Elements

Informal description

Let $\alpha$ be a type equipped with a uniform space structure $u$, and let $\mathfrak{U}[u]$ be the uniformity filter on $\alpha \times \alpha$ with a basis $\{s_i\}_{i \in \iota}$ indexed by $\iota$ and satisfying a predicate $p$. Then the uniform space structure $u$ is trivial (i.e., $u = \bot$) if and only if there exists an index $i \in \iota$ such that $p(i)$ holds and the relation $(x, y) \notin s_i$ holds for all distinct pairs $(x, y) \in \alpha \times \alpha$.

UniformSpace.toTopologicalSpace_bot theorem

: @UniformSpace.toTopologicalSpace α ⊥ = ⊥

Full source

theorem toTopologicalSpace_bot : @UniformSpace.toTopologicalSpace α ⊥ = ⊥ := rfl

Trivial Uniformity Induces Discrete Topology

Informal description

The topology induced by the trivial uniform space structure on a type $\alpha$ is the trivial (discrete) topology.

UniformSpace.toTopologicalSpace_top theorem

: @UniformSpace.toTopologicalSpace α ⊤ = ⊤

Full source

theorem toTopologicalSpace_top : @UniformSpace.toTopologicalSpace α ⊤ = ⊤ := rfl

Topology Induced by Greatest Uniform Space is Trivial

Informal description

The topology induced by the greatest uniform space structure on a type $\alpha$ is the trivial (discrete) topology.

UniformSpace.toTopologicalSpace_iInf theorem

{ι : Sort*} {u : ι → UniformSpace α} : (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace

Full source

theorem toTopologicalSpace_iInf {ι : Sort*} {u : ι → UniformSpace α} :
    (iInf u).toTopologicalSpace = ⨅ i, (u i).toTopologicalSpace :=
  TopologicalSpace.ext_nhds fun a ↦ by simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
    iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]

Infimum of Uniform Spaces Induces Infimum of Topologies

Informal description

For any indexed family of uniform space structures $(u_i)_{i \in \iota}$ on a type $\alpha$, the topology induced by the infimum uniform space $\bigsqcap_i u_i$ is equal to the infimum of the topologies induced by each $u_i$. That is, \[ \text{toTopologicalSpace}\left(\bigsqcap_{i \in \iota} u_i\right) = \bigsqcap_{i \in \iota} \text{toTopologicalSpace}(u_i). \]

UniformSpace.toTopologicalSpace_sInf theorem

{s : Set (UniformSpace α)} : (sInf s).toTopologicalSpace = ⨅ i ∈ s, @UniformSpace.toTopologicalSpace α i

Full source

theorem toTopologicalSpace_sInf {s : Set (UniformSpace α)} :
    (sInf s).toTopologicalSpace = ⨅ i ∈ s, @UniformSpace.toTopologicalSpace α i := by
  rw [sInf_eq_iInf]
  simp only [← toTopologicalSpace_iInf]

Infimum of Uniform Spaces Induces Infimum of Topologies (Set Version)

Informal description

For any set $s$ of uniform space structures on a type $\alpha$, the topology induced by the infimum of $s$ is equal to the infimum of the topologies induced by each uniform space in $s$. That is, \[ \text{toTopologicalSpace}\left(\bigsqcap_{u \in s} u\right) = \bigsqcap_{u \in s} \text{toTopologicalSpace}(u). \]

UniformSpace.toTopologicalSpace_inf theorem

{u v : UniformSpace α} : (u ⊓ v).toTopologicalSpace = u.toTopologicalSpace ⊓ v.toTopologicalSpace

Full source

theorem toTopologicalSpace_inf {u v : UniformSpace α} :
    (u ⊓ v).toTopologicalSpace = u.toTopologicalSpace ⊓ v.toTopologicalSpace :=
  rfl

Infimum of Uniform Spaces Induces Infimum of Topologies

Informal description

For any two uniform space structures $u$ and $v$ on a type $\alpha$, the topological space induced by the infimum of $u$ and $v$ is equal to the infimum of the topological spaces induced by $u$ and $v$ individually. In other words, $(u ⊓ v).\text{toTopologicalSpace} = u.\text{toTopologicalSpace} ⊓ v.\text{toTopologicalSpace}$.

UniformContinuous.continuous theorem

[UniformSpace α] [UniformSpace β] {f : α → β} (hf : UniformContinuous f) : Continuous f

Full source

theorem UniformContinuous.continuous [UniformSpace α] [UniformSpace β] {f : α → β}
    (hf : UniformContinuous f) : Continuous f :=
  continuous_iff_le_induced.mpr <| UniformSpace.toTopologicalSpace_mono <|
    uniformContinuous_iff.1 hf

Uniform continuity implies continuity

Informal description

Let $\alpha$ and $\beta$ be uniform spaces. If a function $f \colon \alpha \to \beta$ is uniformly continuous, then it is continuous.

ULift.uniformSpace instance

[UniformSpace α] : UniformSpace (ULift α)

Full source

/-- Uniform space structure on `ULift α`. -/
instance ULift.uniformSpace [UniformSpace α] : UniformSpace (ULift α) :=
  UniformSpace.comap ULift.down ‹_›

Uniform Space Structure on Lifted Types

Informal description

For any uniform space $\alpha$, the lifted type $\text{ULift}\,\alpha$ carries a natural uniform space structure inherited from $\alpha$.

OrderDual.instUniformSpace instance

[UniformSpace α] : UniformSpace (αᵒᵈ)

Full source

/-- Uniform space structure on `αᵒᵈ`. -/
instance OrderDual.instUniformSpace [UniformSpace α] : UniformSpace (αᵒᵈ) :=
  ‹UniformSpace α›

Uniform Space Structure on Order Duals

Informal description

For any uniform space $\alpha$, the order dual $\alpha^{\text{op}}$ (obtained by reversing the order) also carries a natural uniform space structure, where the uniformity is inherited from $\alpha$.

UniformContinuous.inf_rng theorem

 {f : α → β} {u₁ : UniformSpace α} {u₂ u₃ : UniformSpace β} (h₁ : UniformContinuous[u₁, u₂] f)
  (h₂ : UniformContinuous[u₁, u₃] f) : UniformContinuous[u₁, u₂ ⊓ u₃] f

Full source

theorem UniformContinuous.inf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ u₃ : UniformSpace β}
    (h₁ : UniformContinuous[u₁, u₂] f) (h₂ : UniformContinuous[u₁, u₃] f) :
    UniformContinuous[u₁, u₂ ⊓ u₃] f :=
  tendsto_inf.mpr ⟨h₁, h₂⟩

Uniform continuity is preserved under infimum of target uniform structures

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces, and let $u_1$ be a uniform space structure on $\alpha$, and $u_2, u_3$ be uniform space structures on $\beta$. If $f$ is uniformly continuous with respect to $u_1$ and $u_2$, and also with respect to $u_1$ and $u_3$, then $f$ is uniformly continuous with respect to $u_1$ and the infimum $u_2 \sqcap u_3$ of the uniform structures on $\beta$.

UniformContinuous.inf_dom_left theorem

 {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β} (hf : UniformContinuous[u₁, u₃] f) :
  UniformContinuous[u₁ ⊓ u₂, u₃] f

Full source

theorem UniformContinuous.inf_dom_left {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β}
    (hf : UniformContinuous[u₁, u₃] f) : UniformContinuous[u₁ ⊓ u₂, u₃] f :=
  tendsto_inf_left hf

Uniform continuity preserved under infimum of domain uniformities

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces. If $f$ is uniformly continuous with respect to the uniformities $u_1$ on $\alpha$ and $u_3$ on $\beta$, then $f$ remains uniformly continuous when $\alpha$ is equipped with the infimum uniformity $u_1 \sqcap u_2$ (for any uniformity $u_2$ on $\alpha$) and $\beta$ is equipped with $u_3$.

UniformContinuous.inf_dom_right theorem

 {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β} (hf : UniformContinuous[u₂, u₃] f) :
  UniformContinuous[u₁ ⊓ u₂, u₃] f

Full source

theorem UniformContinuous.inf_dom_right {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β}
    (hf : UniformContinuous[u₂, u₃] f) : UniformContinuous[u₁ ⊓ u₂, u₃] f :=
  tendsto_inf_right hf

Uniform continuity is preserved under infimum of domain uniform structures (right variant)

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces, and let $u_1, u_2$ be uniform space structures on $\alpha$ and $u_3$ a uniform space structure on $\beta$. If $f$ is uniformly continuous with respect to $u_2$ and $u_3$, then $f$ is also uniformly continuous with respect to the infimum uniform space structure $u_1 \sqcap u_2$ on $\alpha$ and $u_3$ on $\beta$.

uniformContinuous_sInf_dom theorem

 {f : α → β} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β} {u : UniformSpace α} (h₁ : u ∈ u₁)
  (hf : UniformContinuous[u, u₂] f) : UniformContinuous[sInf u₁, u₂] f

Full source

theorem uniformContinuous_sInf_dom {f : α → β} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β}
    {u : UniformSpace α} (h₁ : u ∈ u₁) (hf : UniformContinuous[u, u₂] f) :
    UniformContinuous[sInf u₁, u₂] f := by
  delta UniformContinuous
  rw [sInf_eq_iInf', iInf_uniformity]
  exact tendsto_iInf' ⟨u, h₁⟩ hf

Uniform Continuity Preserved Under Infimum of Domain Uniform Structures

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces, and let $u_1$ be a set of uniform space structures on $\alpha$. If $u$ is a uniform space structure in $u_1$ and $f$ is uniformly continuous with respect to $u$ and a fixed uniform space structure $u_2$ on $\beta$, then $f$ is also uniformly continuous with respect to the infimum uniform space structure $\bigsqcap u_1$ on $\alpha$ and $u_2$ on $\beta$.

uniformContinuous_sInf_rng theorem

 {f : α → β} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)} :
  UniformContinuous[u₁, sInf u₂] f ↔ ∀ u ∈ u₂, UniformContinuous[u₁, u] f

Full source

theorem uniformContinuous_sInf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)} :
    UniformContinuous[u₁, sInf u₂]UniformContinuous[u₁, sInf u₂] f ↔ ∀ u ∈ u₂, UniformContinuous[u₁, u] f := by
  delta UniformContinuous
  rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]

Uniform Continuity Criterion for Infimum of Codomain Uniform Structures

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces, where $\alpha$ is equipped with a uniform space structure $u_1$ and $\beta$ is equipped with a set of uniform space structures $u_2$. Then $f$ is uniformly continuous with respect to $u_1$ and the infimum uniform space structure $\bigsqcap u_2$ if and only if for every uniform space structure $u \in u_2$, $f$ is uniformly continuous with respect to $u_1$ and $u$. In other words: \[ f \text{ is uniformly continuous } (u_1, \bigsqcap u_2) \iff \forall u \in u_2, f \text{ is uniformly continuous } (u_1, u). \]

uniformContinuous_iInf_dom theorem

 {f : α → β} {u₁ : ι → UniformSpace α} {u₂ : UniformSpace β} {i : ι} (hf : UniformContinuous[u₁ i, u₂] f) :
  UniformContinuous[iInf u₁, u₂] f

Full source

theorem uniformContinuous_iInf_dom {f : α → β} {u₁ : ι → UniformSpace α} {u₂ : UniformSpace β}
    {i : ι} (hf : UniformContinuous[u₁ i, u₂] f) : UniformContinuous[iInf u₁, u₂] f := by
  delta UniformContinuous
  rw [iInf_uniformity]
  exact tendsto_iInf' i hf

Uniform Continuity Preserved Under Infimum of Domain Uniform Structures

Informal description

Let $\alpha$ and $\beta$ be types equipped with uniform space structures, and let $f \colon \alpha \to \beta$ be a function. Suppose $(u_i)_{i \in \iota}$ is a family of uniform space structures on $\alpha$ and $u_2$ is a uniform space structure on $\beta$. If $f$ is uniformly continuous with respect to $u_i$ and $u_2$ for some $i \in \iota$, then $f$ is uniformly continuous with respect to the infimum uniform space $\bigsqcap_{i \in \iota} u_i$ and $u_2$.

uniformContinuous_iInf_rng theorem

 {f : α → β} {u₁ : UniformSpace α} {u₂ : ι → UniformSpace β} :
  UniformContinuous[u₁, iInf u₂] f ↔ ∀ i, UniformContinuous[u₁, u₂ i] f

Full source

theorem uniformContinuous_iInf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ : ι → UniformSpace β} :
    UniformContinuous[u₁, iInf u₂]UniformContinuous[u₁, iInf u₂] f ↔ ∀ i, UniformContinuous[u₁, u₂ i] f := by
  delta UniformContinuous
  rw [iInf_uniformity, tendsto_iInf]

Uniform Continuity Criterion for Infimum Uniform Structure on Codomain

Informal description

Let $f \colon \alpha \to \beta$ be a function between uniform spaces, where $\alpha$ is equipped with a uniform structure $u_1$ and $\beta$ is equipped with the infimum uniform structure $\bigsqcap_i u_2^i$ of a family $(u_2^i)_{i \in \iota}$. Then $f$ is uniformly continuous if and only if for every index $i$, the function $f$ is uniformly continuous with respect to the uniform structures $u_1$ on $\alpha$ and $u_2^i$ on $\beta$.

discreteTopology_of_discrete_uniformity theorem

[hα : UniformSpace α] (h : uniformity α = 𝓟 idRel) : DiscreteTopology α

Full source

/-- A uniform space with the discrete uniformity has the discrete topology. -/
theorem discreteTopology_of_discrete_uniformity [hα : UniformSpace α] (h : uniformity α = 𝓟 idRel) :
    DiscreteTopology α :=
  ⟨(UniformSpace.ext h.symm : ⊥ = hα) ▸ rfl⟩

Discrete Topology from Discrete Uniformity

Informal description

Let $\alpha$ be a uniform space with uniformity filter $\mathfrak{U}(\alpha)$. If $\mathfrak{U}(\alpha)$ is equal to the principal filter generated by the identity relation $\{(x, x) \mid x \in \alpha\}$, then the topology induced by this uniform structure is the discrete topology.

instUniformSpaceEmpty instance

: UniformSpace Empty

Full source

instance : UniformSpace Empty := ⊥

Uniform Space Structure on the Empty Set

Informal description

The empty set $\emptyset$ is equipped with the trivial uniform space structure.

instUniformSpacePUnit instance

: UniformSpace PUnit

Full source

instance : UniformSpace PUnit := ⊥

Uniform Space Structure on the Singleton Type

Informal description

The type `PUnit` (the singleton type) is equipped with the canonical uniform space structure.

instUniformSpaceBool instance

: UniformSpace Bool

Full source

instance : UniformSpace Bool := ⊥

Uniform Space Structure on Boolean Values

Informal description

The Boolean type `Bool` is equipped with a canonical uniform space structure.

instUniformSpaceNat instance

: UniformSpace ℕ

Full source

instance : UniformSpace ℕ := ⊥

The Uniform Space Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ are equipped with a canonical uniform space structure.

instUniformSpaceInt instance

: UniformSpace ℤ

Full source

instance : UniformSpace ℤ := ⊥

The Uniform Space Structure on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical uniform space structure.

instUniformSpaceAdditive instance

: UniformSpace (Additive α)

Full source

instance : UniformSpace (Additive α) := ‹UniformSpace α›

Uniform Space Structure on Additive Groups

Informal description

For any type $\alpha$ with a uniform space structure, the additive version $\text{Additive}\,\alpha$ inherits a uniform space structure where the uniformity is defined via the additive group structure.

instUniformSpaceMultiplicative instance

: UniformSpace (Multiplicative α)

Full source

instance : UniformSpace (Multiplicative α) := ‹UniformSpace α›

Uniform Space Structure on Multiplicative Groups

Informal description

For any type $\alpha$ with a uniform space structure, the multiplicative version $\text{Multiplicative}\,\alpha$ inherits a uniform space structure where the uniformity is defined via the multiplicative group structure.

uniformContinuous_ofMul theorem

: UniformContinuous (ofMul : α → Additive α)

Full source

theorem uniformContinuous_ofMul : UniformContinuous (ofMul : α → Additive α) :=
  uniformContinuous_id

Uniform Continuity of the Additive Conversion Map

Informal description

The canonical map $\text{ofMul} \colon \alpha \to \text{Additive}\,\alpha$, which sends an element of $\alpha$ to its additive counterpart, is uniformly continuous when both $\alpha$ and $\text{Additive}\,\alpha$ are equipped with their respective uniform space structures.

uniformContinuous_toMul theorem

: UniformContinuous (toMul : Additive α → α)

Full source

theorem uniformContinuous_toMul : UniformContinuous (toMul : Additive α → α) :=
  uniformContinuous_id

Uniform Continuity of the Canonical Map from Additive to Multiplicative Uniform Space

Informal description

The canonical map $\text{toMul} \colon \text{Additive}\,\alpha \to \alpha$ from the additive version of a uniform space $\alpha$ to $\alpha$ itself is uniformly continuous. That is, for every entourage $V$ in the uniformity of $\alpha$, there exists an entourage $U$ in the uniformity of $\text{Additive}\,\alpha$ such that for all pairs $(x, y) \in U$, the pair $(\text{toMul}(x), \text{toMul}(y))$ belongs to $V$.

uniformContinuous_ofAdd theorem

: UniformContinuous (ofAdd : α → Multiplicative α)

Full source

theorem uniformContinuous_ofAdd : UniformContinuous (ofAdd : α → Multiplicative α) :=
  uniformContinuous_id

Uniform Continuity of Additive-to-Multiplicative Conversion

Informal description

The function $\text{ofAdd} \colon \alpha \to \text{Multiplicative}\,\alpha$, which converts elements from an additive uniform space $\alpha$ to its multiplicative counterpart, is uniformly continuous. That is, for every entourage $V$ in the uniformity of $\text{Multiplicative}\,\alpha$, there exists an entourage $U$ in the uniformity of $\alpha$ such that for all pairs $(x, y) \in U$, the pair $(\text{ofAdd}(x), \text{ofAdd}(y))$ belongs to $V$.

uniformContinuous_toAdd theorem

: UniformContinuous (toAdd : Multiplicative α → α)

Full source

theorem uniformContinuous_toAdd : UniformContinuous (toAdd : Multiplicative α → α) :=
  uniformContinuous_id

Uniform Continuity of Multiplicative-to-Additive Conversion

Informal description

The function $\text{toAdd} \colon \text{Multiplicative}\,\alpha \to \alpha$, which converts from the multiplicative group structure to the original additive structure, is uniformly continuous with respect to the uniform space structures on $\text{Multiplicative}\,\alpha$ and $\alpha$.

uniformity_additive theorem

: 𝓤 (Additive α) = (𝓤 α).map (Prod.map ofMul ofMul)

Full source

theorem uniformity_additive : 𝓤 (Additive α) = (𝓤 α).map (Prod.map ofMul ofMul) := rfl

Uniformity of Additive Group via Multiplicative Conversion

Informal description

For a uniform space $\alpha$, the uniformity on the additive version $\text{Additive}\,\alpha$ is equal to the image of the uniformity on $\alpha$ under the map that applies the additive-to-multiplicative conversion $\text{ofMul}$ componentwise to pairs in $\alpha \times \alpha$. In other words, the uniformity $\mathfrak{U}(\text{Additive}\,\alpha)$ is obtained by transforming the uniformity $\mathfrak{U}(\alpha)$ via the map $(x, y) \mapsto (\text{ofMul}\,x, \text{ofMul}\,y)$.

uniformity_multiplicative theorem

: 𝓤 (Multiplicative α) = (𝓤 α).map (Prod.map ofAdd ofAdd)

Full source

theorem uniformity_multiplicative : 𝓤 (Multiplicative α) = (𝓤 α).map (Prod.map ofAdd ofAdd) := rfl

Uniformity of Multiplicative Group via Additive Conversion

Informal description

For a uniform space $\alpha$, the uniformity on the multiplicative version $\text{Multiplicative}\,\alpha$ is equal to the image of the uniformity on $\alpha$ under the map that applies the multiplicative-to-additive conversion $\text{ofAdd}$ componentwise to pairs in $\alpha \times \alpha$. In other words, the uniformity $\mathfrak{U}(\text{Multiplicative}\,\alpha)$ is obtained by transforming the uniformity $\mathfrak{U}(\alpha)$ via the map $(x, y) \mapsto (\text{ofAdd}\,x, \text{ofAdd}\,y)$.

instUniformSpaceSubtype instance

{p : α → Prop} [t : UniformSpace α] : UniformSpace (Subtype p)

Full source

instance instUniformSpaceSubtype {p : α → Prop} [t : UniformSpace α] : UniformSpace (Subtype p) :=
  UniformSpace.comap Subtype.val t

Uniform Space Structure on Subtypes

Informal description

For any type $\alpha$ with a uniform space structure and a predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a uniform space structure where the uniformity is induced by the inclusion map into $\alpha$.

uniformity_subtype theorem

 {p : α → Prop} [UniformSpace α] : 𝓤 (Subtype p) = comap (fun q : Subtype p × Subtype p => (q.1.1, q.2.1)) (𝓤 α)

Full source

theorem uniformity_subtype {p : α → Prop} [UniformSpace α] :
    𝓤 (Subtype p) = comap (fun q : SubtypeSubtype p × Subtype p => (q.1.1, q.2.1)) (𝓤 α) :=
  rfl

Uniformity on Subtype as Preimage of Parent Uniformity

Informal description

For a uniform space $\alpha$ and a predicate $p$ on $\alpha$, the uniformity on the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the preimage of the uniformity on $\alpha$ under the map $(q_1, q_2) \mapsto (q_1.1, q_2.1)$, where $q_1$ and $q_2$ are elements of the subtype.

uniformity_setCoe theorem

{s : Set α} [UniformSpace α] : 𝓤 s = comap (Prod.map ((↑) : s → α) ((↑) : s → α)) (𝓤 α)

Full source

theorem uniformity_setCoe {s : Set α} [UniformSpace α] :
    𝓤 s = comap (Prod.map ((↑) : s → α) ((↑) : s → α)) (𝓤 α) :=
  rfl

Uniformity on Subset as Preimage of Ambient Uniformity

Informal description

For any subset $s$ of a uniform space $\alpha$, the uniformity $\mathfrak{U}(s)$ on $s$ is equal to the preimage of the uniformity $\mathfrak{U}(\alpha)$ under the map $(x, y) \mapsto (x, y)$, where $x, y \in s$ are considered as elements of $\alpha$.

map_uniformity_set_coe theorem

{s : Set α} [UniformSpace α] : map (Prod.map (↑) (↑)) (𝓤 s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)

Full source

theorem map_uniformity_set_coe {s : Set α} [UniformSpace α] :
    map (Prod.map (↑) (↑)) (𝓤 s) = 𝓤𝓤 α ⊓ 𝓟 (s ×ˢ s) := by
  rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]

Image of Subset Uniformity under Inclusion Equals Intersection with Product Set

Informal description

For any subset $s$ of a uniform space $\alpha$, the image of the uniformity $\mathfrak{U}(s)$ under the product map $(x, y) \mapsto (x, y)$ (where $x, y \in s$ are considered as elements of $\alpha$) is equal to the intersection of the uniformity $\mathfrak{U}(\alpha)$ with the principal filter generated by the product set $s \times s$.

uniformContinuous_subtype_val theorem

{p : α → Prop} [UniformSpace α] : UniformContinuous (Subtype.val : { a : α // p a } → α)

Full source

theorem uniformContinuous_subtype_val {p : α → Prop} [UniformSpace α] :
    UniformContinuous (Subtype.val : { a : α // p a } → α) :=
  uniformContinuous_comap

Uniform Continuity of Subtype Inclusion

Informal description

For any uniform space $\alpha$ and a predicate $p$ on $\alpha$, the inclusion map from the subtype $\{x \in \alpha \mid p(x)\}$ to $\alpha$ is uniformly continuous.

UniformContinuous.subtype_mk theorem

 {p : α → Prop} [UniformSpace α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (h : ∀ x, p (f x)) :
  UniformContinuous (fun x => ⟨f x, h x⟩ : β → Subtype p)

Full source

theorem UniformContinuous.subtype_mk {p : α → Prop} [UniformSpace α] [UniformSpace β] {f : β → α}
    (hf : UniformContinuous f) (h : ∀ x, p (f x)) :
    UniformContinuous (fun x => ⟨f x, h x⟩ : β → Subtype p) :=
  uniformContinuous_comap' hf

Uniform Continuity of Subtype Construction from Uniformly Continuous Function

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $f \colon \beta \to \alpha$ be a uniformly continuous function. If $p$ is a predicate on $\alpha$ such that $p(f(x))$ holds for all $x \in \beta$, then the function $x \mapsto \langle f(x), h(x) \rangle$ from $\beta$ to the subtype $\{a \in \alpha \mid p(a)\}$ is uniformly continuous, where $h(x)$ is the proof that $p(f(x))$ holds.

uniformContinuousOn_iff_restrict theorem

 [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ UniformContinuous (s.restrict f)

Full source

theorem uniformContinuousOn_iff_restrict [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} :
    UniformContinuousOnUniformContinuousOn f s ↔ UniformContinuous (s.restrict f) := by
  delta UniformContinuousOn UniformContinuous
  rw [← map_uniformity_set_coe, tendsto_map'_iff]; rfl

Uniform Continuity on Subset is Equivalent to Uniform Continuity of Restriction

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $f \colon \alpha \to \beta$ be a function. For any subset $s \subseteq \alpha$, the function $f$ is uniformly continuous on $s$ if and only if the restriction of $f$ to $s$, denoted $f|_s \colon s \to \beta$, is uniformly continuous.

tendsto_of_uniformContinuous_subtype theorem

 [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} {a : α} (hf : UniformContinuous fun x : s => f x.val)
  (ha : s ∈ 𝓝 a) : Tendsto f (𝓝 a) (𝓝 (f a))

Full source

theorem tendsto_of_uniformContinuous_subtype [UniformSpace α] [UniformSpace β] {f : α → β}
    {s : Set α} {a : α} (hf : UniformContinuous fun x : s => f x.val) (ha : s ∈ 𝓝 a) :
    Tendsto f (𝓝 a) (𝓝 (f a)) := by
  rw [(@map_nhds_subtype_coe_eq_nhds α _ s a (mem_of_mem_nhds ha) ha).symm]
  exact tendsto_map' hf.continuous.continuousAt

Continuity at a Point via Uniform Continuity on a Neighborhood Subset

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $f \colon \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. If the restriction $f|_s \colon s \to \beta$ is uniformly continuous and $s$ is a neighborhood of a point $a \in \alpha$, then $f$ is continuous at $a$, i.e., $f(x) \to f(a)$ as $x \to a$.

UniformContinuousOn.continuousOn theorem

[UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} (h : UniformContinuousOn f s) : ContinuousOn f s

Full source

theorem UniformContinuousOn.continuousOn [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α}
    (h : UniformContinuousOn f s) : ContinuousOn f s := by
  rw [uniformContinuousOn_iff_restrict] at h
  rw [continuousOn_iff_continuous_restrict]
  exact h.continuous

Uniform continuity on a subset implies continuity on that subset

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $f \colon \alpha \to \beta$ be a function. If $f$ is uniformly continuous on a subset $s \subseteq \alpha$, then $f$ is continuous on $s$.

instUniformSpaceMulOpposite instance

[UniformSpace α] : UniformSpace αᵐᵒᵖ

Full source

@[to_additive]
instance [UniformSpace α] : UniformSpace αᵐᵒᵖ :=
  UniformSpace.comap MulOpposite.unop ‹_›

Uniform Space Structure on the Multiplicative Opposite

Informal description

For any uniform space $\alpha$, the multiplicative opposite $\alpha^{\mathrm{op}}$ inherits a uniform space structure where the uniformity is defined via the preimage of the original uniformity under the map $(x, y) \mapsto (x^{\mathrm{op}}, y^{\mathrm{op}})$.

uniformity_mulOpposite theorem

[UniformSpace α] : 𝓤 αᵐᵒᵖ = comap (fun q : αᵐᵒᵖ × αᵐᵒᵖ => (q.1.unop, q.2.unop)) (𝓤 α)

Full source

@[to_additive]
theorem uniformity_mulOpposite [UniformSpace α] :
    𝓤 αᵐᵒᵖ = comap (fun q : αᵐᵒᵖαᵐᵒᵖ × αᵐᵒᵖ => (q.1.unop, q.2.unop)) (𝓤 α) :=
  rfl

Uniformity of Multiplicative Opposite Equals Preimage of Original Uniformity

Informal description

For any uniform space $\alpha$, the uniformity $\mathfrak{U}(\alpha^{\mathrm{op}})$ on the multiplicative opposite $\alpha^{\mathrm{op}}$ is equal to the preimage of the uniformity $\mathfrak{U}(\alpha)$ under the map $(q_1, q_2) \mapsto (q_1^{\mathrm{unop}}, q_2^{\mathrm{unop}})$, where $q_1^{\mathrm{unop}}$ and $q_2^{\mathrm{unop}}$ are the unopposite operations applied to $q_1$ and $q_2$ respectively.

comap_uniformity_mulOpposite theorem

[UniformSpace α] : comap (fun p : α × α => (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α

Full source

@[to_additive (attr := simp)]
theorem comap_uniformity_mulOpposite [UniformSpace α] :
    comap (fun p : α × α => (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α := by
  simpa [uniformity_mulOpposite, comap_comap, (· ∘ ·)] using comap_id

Preimage of Uniformity under Opposite Map Equals Original Uniformity

Informal description

For any uniform space $\alpha$, the preimage of the uniformity filter $\mathfrak{U}(\alpha^{\mathrm{op}})$ under the map $(x, y) \mapsto (x^{\mathrm{op}}, y^{\mathrm{op}})$ is equal to the uniformity filter $\mathfrak{U}(\alpha)$ of the original space.

MulOpposite.uniformContinuous_unop theorem

[UniformSpace α] : UniformContinuous (unop : αᵐᵒᵖ → α)

Full source

@[to_additive]
theorem uniformContinuous_unop [UniformSpace α] : UniformContinuous (unop : αᵐᵒᵖ → α) :=
  uniformContinuous_comap

Uniform Continuity of the Unop Function on Multiplicative Opposite

Informal description

For any uniform space $\alpha$, the function $\mathrm{unop} \colon \alpha^{\mathrm{op}} \to \alpha$ (which sends an element of the multiplicative opposite to its original) is uniformly continuous.

MulOpposite.uniformContinuous_op theorem

[UniformSpace α] : UniformContinuous (op : α → αᵐᵒᵖ)

Full source

@[to_additive]
theorem uniformContinuous_op [UniformSpace α] : UniformContinuous (op : α → αᵐᵒᵖ) :=
  uniformContinuous_comap' uniformContinuous_id

Uniform Continuity of the Opposite Map in Uniform Spaces

Informal description

For any uniform space $\alpha$, the canonical map $\mathrm{op} \colon \alpha \to \alpha^{\mathrm{op}}$ is uniformly continuous, where $\alpha^{\mathrm{op}}$ is equipped with the uniform space structure inherited from $\alpha$.

instUniformSpaceProd instance

[u₁ : UniformSpace α] [u₂ : UniformSpace β] : UniformSpace (α × β)

Full source

instance instUniformSpaceProd [u₁ : UniformSpace α] [u₂ : UniformSpace β] : UniformSpace (α × β) :=
  u₁.comap Prod.fst ⊓ u₂.comap Prod.snd

Uniform Space Structure on Product Spaces

Informal description

Given two uniform spaces $\alpha$ and $\beta$, the product space $\alpha \times \beta$ is equipped with a canonical uniform space structure. The uniformity on $\alpha \times \beta$ is defined as the infimum of the pullbacks of the uniformities on $\alpha$ and $\beta$ under the projection maps $\pi_1 \colon \alpha \times \beta \to \alpha$ and $\pi_2 \colon \alpha \times \beta \to \beta$.

uniformity_prod theorem

 [UniformSpace α] [UniformSpace β] :
  𝓤 (α × β) =
    ((𝓤 α).comap fun p : (α × β) × α × β => (p.1.1, p.2.1)) ⊓ (𝓤 β).comap fun p : (α × β) × α × β => (p.1.2, p.2.2)

Full source

theorem uniformity_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) =
      ((𝓤 α).comap fun p : (α × β) × α × β => (p.1.1, p.2.1)) ⊓
        (𝓤 β).comap fun p : (α × β) × α × β => (p.1.2, p.2.2) :=
  rfl

Product Uniformity as Infimum of Projection Pullbacks

Informal description

For uniform spaces $\alpha$ and $\beta$, the uniformity $\mathfrak{U}(\alpha \times \beta)$ on the product space $\alpha \times \beta$ is equal to the infimum of: 1. The pullback of $\mathfrak{U}(\alpha)$ under the projection $(p_1, p_2) \mapsto (p_{1.1}, p_{2.1})$, and 2. The pullback of $\mathfrak{U}(\beta)$ under the projection $(p_1, p_2) \mapsto (p_{1.2}, p_{2.2})$.

instIsCountablyGeneratedProdUniformity instance

 [UniformSpace α] [IsCountablyGenerated (𝓤 α)] [UniformSpace β] [IsCountablyGenerated (𝓤 β)] :
  IsCountablyGenerated (𝓤 (α × β))

Full source

instance [UniformSpace α] [IsCountablyGenerated (𝓤 α)]
    [UniformSpace β] [IsCountablyGenerated (𝓤 β)] : IsCountablyGenerated (𝓤 (α × β)) := by
  rw [uniformity_prod]
  infer_instance

Countable Generation of Product Uniformity

Informal description

For uniform spaces $\alpha$ and $\beta$ with countably generated uniformities $\mathfrak{U}(\alpha)$ and $\mathfrak{U}(\beta)$, the product uniformity $\mathfrak{U}(\alpha \times \beta)$ is also countably generated.

uniformity_prod_eq_comap_prod theorem

 [UniformSpace α] [UniformSpace β] :
  𝓤 (α × β) = comap (fun p : (α × β) × α × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β)

Full source

theorem uniformity_prod_eq_comap_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) =
      comap (fun p : (α × β) × α × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β) := by
  simp_rw [uniformity_prod, prod_eq_inf, Filter.comap_inf, Filter.comap_comap, Function.comp_def]

Product Uniformity as Preimage of Component Uniformities

Informal description

For uniform spaces $\alpha$ and $\beta$, the uniformity on the product space $\alpha \times \beta$ is equal to the preimage of the product uniformity $\mathfrak{U}(\alpha) \times \mathfrak{U}(\beta)$ under the map that sends a pair $((x_1, y_1), (x_2, y_2))$ to $((x_1, x_2), (y_1, y_2))$.

uniformity_prod_eq_prod theorem

 [UniformSpace α] [UniformSpace β] :
  𝓤 (α × β) = map (fun p : (α × α) × β × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β)

Full source

theorem uniformity_prod_eq_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) = map (fun p : (α × α) × β × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β) := by
  rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]

Product Uniformity as Image of Component Uniformities

Informal description

For uniform spaces $\alpha$ and $\beta$, the uniformity on the product space $\alpha \times \beta$ is equal to the image of the product filter $\mathfrak{U}(\alpha) \times \mathfrak{U}(\beta)$ under the map that sends a pair $((x_1, x_2), (y_1, y_2))$ to $((x_1, y_1), (x_2, y_2))$.

mem_uniformity_of_uniformContinuous_invariant theorem

 [UniformSpace α] [UniformSpace β] {s : Set (β × β)} {f : α → α → β} (hf : UniformContinuous fun p : α × α => f p.1 p.2)
  (hs : s ∈ 𝓤 β) : ∃ u ∈ 𝓤 α, ∀ a b c, (a, b) ∈ u → (f a c, f b c) ∈ s

Full source

theorem mem_uniformity_of_uniformContinuous_invariant [UniformSpace α] [UniformSpace β]
    {s : Set (β × β)} {f : α → α → β} (hf : UniformContinuous fun p : α × α => f p.1 p.2)
    (hs : s ∈ 𝓤 β) : ∃ u ∈ 𝓤 α, ∀ a b c, (a, b) ∈ u → (f a c, f b c) ∈ s := by
  rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf
  rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩
  exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩

Uniform Continuity Implies Uniform Invariance of Entourages

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $s \subseteq \beta \times \beta$ be an entourage in $\beta$, and $f \colon \alpha \times \alpha \to \beta$ be a uniformly continuous function. Then there exists an entourage $u \subseteq \alpha \times \alpha$ such that for all $a, b, c \in \alpha$, if $(a, b) \in u$, then $(f(a, c), f(b, c)) \in s$.

entourageProd definition

(u : Set (α × α)) (v : Set (β × β)) : Set ((α × β) × α × β)

Full source

/-- An entourage of the diagonal in `α` and an entourage in `β` yield an entourage in `α × β`
once we permute coordinates. -/
def entourageProd (u : Set (α × α)) (v : Set (β × β)) : Set ((α × β) × α × β) :=
  {((a₁, b₁),(a₂, b₂)) | (a₁, a₂) ∈ u ∧ (b₁, b₂) ∈ v}

Product entourage construction

Informal description

Given entourages $u \subseteq \alpha \times \alpha$ and $v \subseteq \beta \times \beta$, the set $\text{entourageProd}(u, v)$ consists of all pairs $((a_1, b_1), (a_2, b_2))$ in $(\alpha \times \beta) \times (\alpha \times \beta)$ such that $(a_1, a_2) \in u$ and $(b_1, b_2) \in v$. This construction permutes the coordinates to form an entourage in the product uniform space $\alpha \times \beta$.

mem_entourageProd theorem

 {u : Set (α × α)} {v : Set (β × β)} {p : (α × β) × α × β} :
  p ∈ entourageProd u v ↔ (p.1.1, p.2.1) ∈ u ∧ (p.1.2, p.2.2) ∈ v

Full source

theorem mem_entourageProd {u : Set (α × α)} {v : Set (β × β)} {p : (α × β) × α × β} :
    p ∈ entourageProd u vp ∈ entourageProd u v ↔ (p.1.1, p.2.1) ∈ u ∧ (p.1.2, p.2.2) ∈ v := Iff.rfl

Characterization of Membership in Product Entourage

Informal description

For any sets $u \subseteq \alpha \times \alpha$ and $v \subseteq \beta \times \beta$, and any pair $p = ((a_1, b_1), (a_2, b_2)) \in (\alpha \times \beta) \times (\alpha \times \beta)$, we have $p \in \text{entourageProd}(u, v)$ if and only if $(a_1, a_2) \in u$ and $(b_1, b_2) \in v$.

entourageProd_mem_uniformity theorem

 [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : Set (α × α)} {v : Set (β × β)} (hu : u ∈ 𝓤 α) (hv : v ∈ 𝓤 β) :
  entourageProd u v ∈ 𝓤 (α × β)

Full source

theorem entourageProd_mem_uniformity [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : Set (α × α)}
    {v : Set (β × β)} (hu : u ∈ 𝓤 α) (hv : v ∈ 𝓤 β) :
    entourageProdentourageProd u v ∈ 𝓤 (α × β) := by
  rw [uniformity_prod]; exact inter_mem_inf (preimage_mem_comap hu) (preimage_mem_comap hv)

Product Entourage Belongs to Product Uniformity

Informal description

For uniform spaces $\alpha$ and $\beta$, if $u$ is an entourage in $\alpha$ and $v$ is an entourage in $\beta$, then the product entourage $\text{entourageProd}(u, v)$ is an entourage in the product uniform space $\alpha \times \beta$.

ball_entourageProd theorem

(u : Set (α × α)) (v : Set (β × β)) (x : α × β) : ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v

Full source

theorem ball_entourageProd (u : Set (α × α)) (v : Set (β × β)) (x : α × β) :
    ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v := by
  ext p; simp only [ball, entourageProd, Set.mem_setOf_eq, Set.mem_prod, Set.mem_preimage]

Uniform Ball Decomposition in Product Space: $\text{ball}(x, u \times v) = \text{ball}(x_1, u) \times \text{ball}(x_2, v)$

Informal description

For any uniform spaces $\alpha$ and $\beta$, given entourages $u \subseteq \alpha \times \alpha$ and $v \subseteq \beta \times \beta$, and any point $x = (x_1, x_2) \in \alpha \times \beta$, the uniform ball centered at $x$ with respect to the product entourage $\text{entourageProd}(u, v)$ is equal to the Cartesian product of the uniform balls centered at $x_1$ with respect to $u$ and at $x_2$ with respect to $v$. In symbols: $$ \text{ball}(x, \text{entourageProd}(u, v)) = \text{ball}(x_1, u) \times \text{ball}(x_2, v). $$

IsSymmetricRel.entourageProd theorem

 {u : Set (α × α)} {v : Set (β × β)} (hu : IsSymmetricRel u) (hv : IsSymmetricRel v) :
  IsSymmetricRel (entourageProd u v)

Full source

lemma IsSymmetricRel.entourageProd {u : Set (α × α)} {v : Set (β × β)}
    (hu : IsSymmetricRel u) (hv : IsSymmetricRel v) :
    IsSymmetricRel (entourageProd u v) :=
  Set.ext fun _ ↦ and_congr hu.mk_mem_comm hv.mk_mem_comm

Symmetry of Product Entourage Relation

Informal description

Let $\alpha$ and $\beta$ be types equipped with uniform structures, and let $u \subseteq \alpha \times \alpha$ and $v \subseteq \beta \times \beta$ be symmetric relations. Then the product relation $\text{entourageProd}(u, v) \subseteq (\alpha \times \beta) \times (\alpha \times \beta)$ is also symmetric.

Filter.HasBasis.uniformity_prod theorem

 {ιa ιb : Type*} [UniformSpace α] [UniformSpace β] {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → Set (α × α)}
  {sb : ιb → Set (β × β)} (ha : (𝓤 α).HasBasis pa sa) (hb : (𝓤 β).HasBasis pb sb) :
  (𝓤 (α × β)).HasBasis (fun i : ιa × ιb ↦ pa i.1 ∧ pb i.2) (fun i ↦ entourageProd (sa i.1) (sb i.2))

Full source

theorem Filter.HasBasis.uniformity_prod {ιa ιb : Type*} [UniformSpace α] [UniformSpace β]
    {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → Set (α × α)} {sb : ιb → Set (β × β)}
    (ha : (𝓤 α).HasBasis pa sa) (hb : (𝓤 β).HasBasis pb sb) :
    (𝓤 (α × β)).HasBasis (fun i : ιa × ιb ↦ pa i.1 ∧ pb i.2)
    (fun i ↦ entourageProd (sa i.1) (sb i.2)) :=
  (ha.comap _).inf (hb.comap _)

Basis Construction for Product Uniformity: $\mathfrak{U}(\alpha \times \beta) = \text{entourageProd}(\mathfrak{U}(\alpha), \mathfrak{U}(\beta))$

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_a\}_{a \in \iota_a}$ indexed by $\iota_a$ with predicate $p_a$, and $\mathfrak{U}(\beta)$ has a basis $\{s_b\}_{b \in \iota_b}$ indexed by $\iota_b$ with predicate $p_b$. Then the uniformity filter $\mathfrak{U}(\alpha \times \beta)$ on the product space has a basis consisting of the sets $\text{entourageProd}(s_a, s_b)$ for $(a,b) \in \iota_a \times \iota_b$ such that $p_a(a)$ and $p_b(b)$ hold.

entourageProd_subset theorem

 [UniformSpace α] [UniformSpace β] {s : Set ((α × β) × α × β)} (h : s ∈ 𝓤 (α × β)) :
  ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Full source

theorem entourageProd_subset [UniformSpace α] [UniformSpace β]
    {s : Set ((α × β) × α × β)} (h : s ∈ 𝓤 (α × β)) :
    ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s := by
  rcases (((𝓤 α).basis_sets.uniformity_prod (𝓤 β).basis_sets).mem_iff' s).1 h with ⟨w, hw⟩
  use w.1, hw.1.1, w.2, hw.1.2, hw.2

Existence of Component Entourages in Product Uniformity

Informal description

For any uniform spaces $\alpha$ and $\beta$, and any entourage $s$ in the product uniformity $\mathfrak{U}(\alpha \times \beta)$, there exist entourages $u \in \mathfrak{U}(\alpha)$ and $v \in \mathfrak{U}(\beta)$ such that the product entourage $\text{entourageProd}(u, v)$ is contained in $s$.

tendsto_prod_uniformity_fst theorem

 [UniformSpace α] [UniformSpace β] : Tendsto (fun p : (α × β) × α × β => (p.1.1, p.2.1)) (𝓤 (α × β)) (𝓤 α)

Full source

theorem tendsto_prod_uniformity_fst [UniformSpace α] [UniformSpace β] :
    Tendsto (fun p : (α × β) × α × β => (p.1.1, p.2.1)) (𝓤 (α × β)) (𝓤 α) :=
  le_trans (map_mono inf_le_left) map_comap_le

Uniform Continuity of First Projection on Product Uniform Space

Informal description

For uniform spaces $\alpha$ and $\beta$, the projection map $\pi_1 \colon (\alpha \times \beta) \times (\alpha \times \beta) \to \alpha \times \alpha$ defined by $( (x_1,y_1), (x_2,y_2) ) \mapsto (x_1,x_2)$ is uniformly continuous. In terms of filters, this means the pushforward of the uniformity $\mathfrak{U}(\alpha \times \beta)$ under $\pi_1$ is contained in the uniformity $\mathfrak{U}(\alpha)$.

tendsto_prod_uniformity_snd theorem

 [UniformSpace α] [UniformSpace β] : Tendsto (fun p : (α × β) × α × β => (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β)

Full source

theorem tendsto_prod_uniformity_snd [UniformSpace α] [UniformSpace β] :
    Tendsto (fun p : (α × β) × α × β => (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β) :=
  le_trans (map_mono inf_le_right) map_comap_le

Continuity of Second Projection in Product Uniformity

Informal description

For any uniform spaces $\alpha$ and $\beta$, the projection map $\pi_2 \colon \alpha \times \beta \to \beta$ induces a continuous map between the uniformity filters. Specifically, the map $(p \mapsto (p_{1.2}, p_{2.2}))$ from $(\alpha \times \beta) \times (\alpha \times \beta)$ to $\beta \times \beta$ sends the uniformity filter $\mathfrak{U}(\alpha \times \beta)$ to the uniformity filter $\mathfrak{U}(\beta)$.

uniformContinuous_fst theorem

[UniformSpace α] [UniformSpace β] : UniformContinuous fun p : α × β => p.1

Full source

theorem uniformContinuous_fst [UniformSpace α] [UniformSpace β] :
    UniformContinuous fun p : α × β => p.1 :=
  tendsto_prod_uniformity_fst

Uniform Continuity of First Projection on Product Space

Informal description

For any uniform spaces $\alpha$ and $\beta$, the first projection map $\pi_1 \colon \alpha \times \beta \to \alpha$ is uniformly continuous.

uniformContinuous_snd theorem

[UniformSpace α] [UniformSpace β] : UniformContinuous fun p : α × β => p.2

Full source

theorem uniformContinuous_snd [UniformSpace α] [UniformSpace β] :
    UniformContinuous fun p : α × β => p.2 :=
  tendsto_prod_uniformity_snd

Uniform Continuity of Second Projection in Product Space

Informal description

For any uniform spaces $\alpha$ and $\beta$, the second projection map $\pi_2 \colon \alpha \times \beta \to \beta$ defined by $\pi_2(p) = p.2$ is uniformly continuous.

UniformContinuous.prodMk theorem

 {f₁ : α → β} {f₂ : α → γ} (h₁ : UniformContinuous f₁) (h₂ : UniformContinuous f₂) :
  UniformContinuous fun a => (f₁ a, f₂ a)

Full source

theorem UniformContinuous.prodMk {f₁ : α → β} {f₂ : α → γ} (h₁ : UniformContinuous f₁)
    (h₂ : UniformContinuous f₂) : UniformContinuous fun a => (f₁ a, f₂ a) := by
  rw [UniformContinuous, uniformity_prod]
  exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩

Uniform continuity of the product map $(f_1, f_2)$

Informal description

Let $f_1 \colon \alpha \to \beta$ and $f_2 \colon \alpha \to \gamma$ be uniformly continuous functions between uniform spaces. Then the function $a \mapsto (f_1(a), f_2(a))$ from $\alpha$ to $\beta \times \gamma$ is uniformly continuous.

UniformContinuous.prodMk_left theorem

{f : α × β → γ} (h : UniformContinuous f) (b) : UniformContinuous fun a => f (a, b)

Full source

theorem UniformContinuous.prodMk_left {f : α × β → γ} (h : UniformContinuous f) (b) :
    UniformContinuous fun a => f (a, b) :=
  h.comp (uniformContinuous_id.prodMk uniformContinuous_const)

Uniform continuity of partial application in first argument

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a uniformly continuous function between uniform spaces, and let $b \in \beta$ be fixed. Then the function $a \mapsto f(a, b)$ from $\alpha$ to $\gamma$ is uniformly continuous.

UniformContinuous.prodMk_right theorem

{f : α × β → γ} (h : UniformContinuous f) (a) : UniformContinuous fun b => f (a, b)

Full source

theorem UniformContinuous.prodMk_right {f : α × β → γ} (h : UniformContinuous f) (a) :
    UniformContinuous fun b => f (a, b) :=
  h.comp (uniformContinuous_const.prodMk uniformContinuous_id)

Uniform continuity in the second argument of a product function

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a uniformly continuous function between uniform spaces. For any fixed $a \in \alpha$, the function $b \mapsto f(a, b)$ from $\beta$ to $\gamma$ is uniformly continuous.

UniformContinuous.prodMap theorem

 [UniformSpace δ] {f : α → γ} {g : β → δ} (hf : UniformContinuous f) (hg : UniformContinuous g) :
  UniformContinuous (Prod.map f g)

Full source

theorem UniformContinuous.prodMap [UniformSpace δ] {f : α → γ} {g : β → δ}
    (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous (Prod.map f g) :=
  (hf.comp uniformContinuous_fst).prodMk (hg.comp uniformContinuous_snd)

Uniform continuity of the product map $f \times g$

Informal description

Let $\alpha$, $\beta$, $\gamma$, and $\delta$ be uniform spaces. If $f \colon \alpha \to \gamma$ and $g \colon \beta \to \delta$ are uniformly continuous functions, then the product map $(f \times g) \colon \alpha \times \beta \to \gamma \times \delta$ defined by $(f \times g)(a, b) = (f(a), g(b))$ is also uniformly continuous.

toTopologicalSpace_prod theorem

 {α} {β} [u : UniformSpace α] [v : UniformSpace β] :
  @UniformSpace.toTopologicalSpace (α × β) instUniformSpaceProd =
    @instTopologicalSpaceProd α β u.toTopologicalSpace v.toTopologicalSpace

Full source

theorem toTopologicalSpace_prod {α} {β} [u : UniformSpace α] [v : UniformSpace β] :
    @UniformSpace.toTopologicalSpace (α × β) instUniformSpaceProd =
      @instTopologicalSpaceProd α β u.toTopologicalSpace v.toTopologicalSpace :=
  rfl

Product Uniform Space Induces Product Topology

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with uniformities $u$ and $v$ respectively. The topology induced by the product uniform space structure on $\alpha \times \beta$ coincides with the product topology obtained from the topologies induced by $u$ on $\alpha$ and $v$ on $\beta$.

uniformContinuous_inf_dom_left₂ theorem

 {α β γ} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}
  (h : by haveI := ua1; haveI := ub1; exact UniformContinuous fun p : α × β => f p.1 p.2) :
  by
  haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2
  exact UniformContinuous fun p : α × β => f p.1 p.2

Full source

/-- A version of `UniformContinuous.inf_dom_left` for binary functions -/
theorem uniformContinuous_inf_dom_left₂ {α β γ} {f : α → β → γ} {ua1 ua2 : UniformSpace α}
    {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}
    (h : by haveI := ua1; haveI := ub1; exact UniformContinuous fun p : α × β => f p.1 p.2) : by
      haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2
      exact UniformContinuous fun p : α × β => f p.1 p.2 := by
  -- proof essentially copied from `continuous_inf_dom_left₂`
  have ha := @UniformContinuous.inf_dom_left _ _ id ua1 ua2 ua1 (@uniformContinuous_id _ (id _))
  have hb := @UniformContinuous.inf_dom_left _ _ id ub1 ub2 ub1 (@uniformContinuous_id _ (id _))
  have h_unif_cont_id :=
    @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua1 ub1 _ _ ha hb
  exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ h h_unif_cont_id

Uniform continuity of binary functions under infimum of domain uniformities (left variant)

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with uniform space structures. Consider a binary function $f \colon \alpha \to \beta \to \gamma$ and uniform space structures $ua_1, ua_2$ on $\alpha$, $ub_1, ub_2$ on $\beta$, and $uc_1$ on $\gamma$. If $f$ is uniformly continuous when $\alpha$ is equipped with $ua_1$ and $\beta$ is equipped with $ub_1$, then $f$ remains uniformly continuous when $\alpha$ is equipped with the infimum uniformity $ua_1 \sqcap ua_2$ and $\beta$ is equipped with the infimum uniformity $ub_1 \sqcap ub_2$.

uniformContinuous_inf_dom_right₂ theorem

 {α β γ} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}
  (h : by haveI := ua2; haveI := ub2; exact UniformContinuous fun p : α × β => f p.1 p.2) :
  by
  haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2
  exact UniformContinuous fun p : α × β => f p.1 p.2

Full source

/-- A version of `UniformContinuous.inf_dom_right` for binary functions -/
theorem uniformContinuous_inf_dom_right₂ {α β γ} {f : α → β → γ} {ua1 ua2 : UniformSpace α}
    {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ}
    (h : by haveI := ua2; haveI := ub2; exact UniformContinuous fun p : α × β => f p.1 p.2) : by
      haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2
      exact UniformContinuous fun p : α × β => f p.1 p.2 := by
  -- proof essentially copied from `continuous_inf_dom_right₂`
  have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
  have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
  have h_unif_cont_id :=
    @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb
  exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ h h_unif_cont_id

Uniform continuity under infimum of domain uniform structures (right variant for binary functions)

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with uniform space structures. Let $f \colon \alpha \to \beta \to \gamma$ be a function. Suppose that when $\alpha$ is given the uniform structure $u_{a2}$ and $\beta$ is given $u_{b2}$, the induced map $(x,y) \mapsto f(x)(y)$ from $\alpha \times \beta$ to $\gamma$ is uniformly continuous. Then, when $\alpha$ is equipped with the infimum uniform structure $u_{a1} \sqcap u_{a2}$ and $\beta$ with $u_{b1} \sqcap u_{b2}$, the map $(x,y) \mapsto f(x)(y)$ remains uniformly continuous.

uniformContinuous_sInf_dom₂ theorem

 {α β γ} {f : α → β → γ} {uas : Set (UniformSpace α)} {ubs : Set (UniformSpace β)} {ua : UniformSpace α}
  {ub : UniformSpace β} {uc : UniformSpace γ} (ha : ua ∈ uas) (hb : ub ∈ ubs)
  (hf : UniformContinuous fun p : α × β => f p.1 p.2) :
  by
  haveI := sInf uas; haveI := sInf ubs
  exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2

Full source

/-- A version of `uniformContinuous_sInf_dom` for binary functions -/
theorem uniformContinuous_sInf_dom₂ {α β γ} {f : α → β → γ} {uas : Set (UniformSpace α)}
    {ubs : Set (UniformSpace β)} {ua : UniformSpace α} {ub : UniformSpace β} {uc : UniformSpace γ}
    (ha : ua ∈ uas) (hb : ub ∈ ubs) (hf : UniformContinuous fun p : α × β => f p.1 p.2) : by
      haveI := sInf uas; haveI := sInf ubs
      exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2 := by
  -- proof essentially copied from `continuous_sInf_dom`
  let _ : UniformSpace (α × β) := instUniformSpaceProd
  have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
  have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
  have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
  exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id

Uniform Continuity of Binary Functions Under Infimum of Domain Uniform Structures

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with uniform space structures. Let $f \colon \alpha \to \beta \to \gamma$ be a function, and let $uas$ and $ubs$ be sets of uniform space structures on $\alpha$ and $\beta$ respectively. Suppose $ua \in uas$ and $ub \in ubs$ are uniform space structures such that the function $(x, y) \mapsto f(x)(y)$ is uniformly continuous from $\alpha \times \beta$ to $\gamma$ with respect to $ua$, $ub$, and a fixed uniform space structure $uc$ on $\gamma$. Then, the same function is also uniformly continuous with respect to the infimum uniform space structures $\bigsqcap uas$ on $\alpha$, $\bigsqcap ubs$ on $\beta$, and $uc$ on $\gamma$.

UniformContinuous₂ definition

(f : α → β → γ)

Full source

/-- Uniform continuity for functions of two variables. -/
def UniformContinuous₂ (f : α → β → γ) :=
  UniformContinuous (uncurry f)

Uniformly continuous function of two variables

Informal description

A function $f \colon \alpha \to \beta \to \gamma$ between uniform spaces is *uniformly continuous in two variables* if the uncurried function $(x, y) \mapsto f(x, y)$ is uniformly continuous with respect to the product uniformity on $\alpha \times \beta$.

uniformContinuous₂_def theorem

(f : α → β → γ) : UniformContinuous₂ f ↔ UniformContinuous (uncurry f)

Full source

theorem uniformContinuous₂_def (f : α → β → γ) :
    UniformContinuous₂UniformContinuous₂ f ↔ UniformContinuous (uncurry f) :=
  Iff.rfl

Uniform Continuity in Two Variables via Uncurrying

Informal description

A function $f \colon \alpha \to \beta \to \gamma$ between uniform spaces is uniformly continuous in two variables if and only if its uncurried version $(x, y) \mapsto f(x, y)$ is uniformly continuous with respect to the product uniformity on $\alpha \times \beta$.

UniformContinuous₂.uniformContinuous theorem

{f : α → β → γ} (h : UniformContinuous₂ f) : UniformContinuous (uncurry f)

Full source

theorem UniformContinuous₂.uniformContinuous {f : α → β → γ} (h : UniformContinuous₂ f) :
    UniformContinuous (uncurry f) :=
  h

Uniform Continuity of Uncurried Function from Uniformly Continuous Bivariate Function

Informal description

If a function $f \colon \alpha \to \beta \to \gamma$ between uniform spaces is uniformly continuous in two variables, then the uncurried function $(x, y) \mapsto f(x, y)$ is uniformly continuous with respect to the product uniformity on $\alpha \times \beta$.

uniformContinuous₂_curry theorem

(f : α × β → γ) : UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f

Full source

theorem uniformContinuous₂_curry (f : α × β → γ) :
    UniformContinuous₂UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f := by
  rw [UniformContinuous₂, uncurry_curry]

Equivalence of Uniform Continuity for Curried and Uncurried Functions

Informal description

For a function $f \colon \alpha \times \beta \to \gamma$ between uniform spaces, the following are equivalent: 1. The curried function $\text{curry}(f) \colon \alpha \to \beta \to \gamma$ is uniformly continuous in two variables. 2. The original function $f$ is uniformly continuous.

UniformContinuous₂.comp theorem

 {f : α → β → γ} {g : γ → δ} (hg : UniformContinuous g) (hf : UniformContinuous₂ f) : UniformContinuous₂ (g ∘₂ f)

Full source

theorem UniformContinuous₂.comp {f : α → β → γ} {g : γ → δ} (hg : UniformContinuous g)
    (hf : UniformContinuous₂ f) : UniformContinuous₂ (g ∘₂ f) :=
  hg.comp hf

Uniform Continuity of Composition of a Uniformly Continuous Function with a Uniformly Continuous Bivariate Function

Informal description

Let $\alpha$, $\beta$, $\gamma$, and $\delta$ be uniform spaces. Given a uniformly continuous function $g \colon \gamma \to \delta$ and a function $f \colon \alpha \to \beta \to \gamma$ that is uniformly continuous in two variables, the composition $g \circ₂ f \colon \alpha \to \beta \to \delta$ defined by $(g \circ₂ f)(x, y) = g(f(x, y))$ is also uniformly continuous in two variables.

UniformContinuous₂.bicompl theorem

 {f : α → β → γ} {ga : δ → α} {gb : δ' → β} (hf : UniformContinuous₂ f) (hga : UniformContinuous ga)
  (hgb : UniformContinuous gb) : UniformContinuous₂ (bicompl f ga gb)

Full source

theorem UniformContinuous₂.bicompl {f : α → β → γ} {ga : δ → α} {gb : δ' → β}
    (hf : UniformContinuous₂ f) (hga : UniformContinuous ga) (hgb : UniformContinuous gb) :
    UniformContinuous₂ (bicompl f ga gb) :=
  hf.uniformContinuous.comp (hga.prodMap hgb)

Uniform Continuity of Bicomposition for Bivariate Functions

Informal description

Let $\alpha$, $\beta$, $\gamma$, $\delta$, and $\delta'$ be uniform spaces. Given a function $f \colon \alpha \to \beta \to \gamma$ that is uniformly continuous in two variables, and uniformly continuous functions $g_a \colon \delta \to \alpha$ and $g_b \colon \delta' \to \beta$, the composition $(x, y) \mapsto f(g_a(x), g_b(y))$ is uniformly continuous in two variables.

toTopologicalSpace_subtype theorem

 [u : UniformSpace α] {p : α → Prop} :
  @UniformSpace.toTopologicalSpace (Subtype p) instUniformSpaceSubtype =
    @instTopologicalSpaceSubtype α p u.toTopologicalSpace

Full source

theorem toTopologicalSpace_subtype [u : UniformSpace α] {p : α → Prop} :
    @UniformSpace.toTopologicalSpace (Subtype p) instUniformSpaceSubtype =
      @instTopologicalSpaceSubtype α p u.toTopologicalSpace :=
  rfl

Subtype Uniform Space Induces Subspace Topology

Informal description

For a uniform space $\alpha$ with uniformity $\mathfrak{U}(\alpha)$ and a predicate $p : \alpha \to \text{Prop}$, the topological space structure induced by the uniform space structure on the subtype $\{x \in \alpha \mid p(x)\}$ coincides with the subspace topology inherited from $\alpha$. In other words, the topology on the subtype $\{x \in \alpha \mid p(x)\}$ obtained from its uniform space structure is the same as the topology induced by the inclusion map into $\alpha$.

Sum.instUniformSpace instance

: UniformSpace (α ⊕ β)

Full source

/-- Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained
by taking independently an entourage of the diagonal in the first part, and an entourage of
the diagonal in the second part. -/
instance Sum.instUniformSpace : UniformSpace (α ⊕ β) where
  uniformity := mapmap (fun p : α × α => (inl p.1, inl p.2)) (𝓤 α) ⊔
    map (fun p : β × β => (inr p.1, inr p.2)) (𝓤 β)
  symm := fun _ hs ↦ ⟨symm_le_uniformity hs.1, symm_le_uniformity hs.2⟩
  comp := fun s hs ↦ by
    rcases comp_mem_uniformity_sets hs.1 with ⟨tα, htα, Htα⟩
    rcases comp_mem_uniformity_sets hs.2 with ⟨tβ, htβ, Htβ⟩
    filter_upwards [mem_lift' (union_mem_sup (image_mem_map htα) (image_mem_map htβ))]
    rintro ⟨_, _⟩ ⟨z, ⟨⟨a, b⟩, hab, ⟨⟩⟩ | ⟨⟨a, b⟩, hab, ⟨⟩⟩, ⟨⟨_, c⟩, hbc, ⟨⟩⟩ | ⟨⟨_, c⟩, hbc, ⟨⟩⟩⟩
    exacts [@Htα (_, _) ⟨b, hab, hbc⟩, @Htβ (_, _) ⟨b, hab, hbc⟩]
  nhds_eq_comap_uniformity x := by
    ext
    cases x <;> simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity,
      Prod.ext_iff]

Uniform Space Structure on Disjoint Union

Informal description

The disjoint union $\alpha \oplus \beta$ of two uniform spaces $\alpha$ and $\beta$ can be equipped with a uniform space structure where the uniformity is generated by the union of the images of the entourages from $\alpha$ and $\beta$ under the left and right inclusion maps respectively. Specifically, the uniformity on $\alpha \oplus \beta$ is the supremum of the filters obtained by pushing forward the uniformities of $\alpha$ and $\beta$ via the inclusion maps.

union_mem_uniformity_sum theorem

 {a : Set (α × α)} (ha : a ∈ 𝓤 α) {b : Set (β × β)} (hb : b ∈ 𝓤 β) :
  Prod.map inl inl '' a ∪ Prod.map inr inr '' b ∈ 𝓤 (α ⊕ β)

Full source

/-- The union of an entourage of the diagonal in each set of a disjoint union is again an entourage
of the diagonal. -/
theorem union_mem_uniformity_sum {a : Set (α × α)} (ha : a ∈ 𝓤 α) {b : Set (β × β)} (hb : b ∈ 𝓤 β) :
    Prod.mapProd.map inl inl '' aProd.map inl inl '' a ∪ Prod.map inr inr '' bProd.map inl inl '' a ∪ Prod.map inr inr '' b ∈ 𝓤 (α ⊕ β) :=
  union_mem_sup (image_mem_map ha) (image_mem_map hb)

Union of Entourages in Disjoint Union Uniform Space

Informal description

For any uniform spaces $\alpha$ and $\beta$, if $a \subseteq \alpha \times \alpha$ is an entourage in $\alpha$ and $b \subseteq \beta \times \beta$ is an entourage in $\beta$, then the union of the images of $a$ and $b$ under the left and right inclusion maps (respectively) is an entourage in the disjoint union uniform space $\alpha \oplus \beta$. More precisely, given $a \in \mathfrak{U}(\alpha)$ and $b \in \mathfrak{U}(\beta)$, we have: \[ \text{Prod.map}(\text{inl}, \text{inl})'' a \cup \text{Prod.map}(\text{inr}, \text{inr})'' b \in \mathfrak{U}(\alpha \oplus \beta) \] where $\text{inl} : \alpha \to \alpha \oplus \beta$ and $\text{inr} : \beta \to \alpha \oplus \beta$ are the inclusion maps, and $\text{Prod.map}(f,g)(x,y) = (f x, g y)$.

Sum.uniformity theorem

: 𝓤 (α ⊕ β) = map (Prod.map inl inl) (𝓤 α) ⊔ map (Prod.map inr inr) (𝓤 β)

Full source

theorem Sum.uniformity : 𝓤 (α ⊕ β) = mapmap (Prod.map inl inl) (𝓤 α) ⊔ map (Prod.map inr inr) (𝓤 β) :=
  rfl

Uniformity of Disjoint Union as Supremum of Pushforwards

Informal description

The uniformity filter on the disjoint union $\alpha \oplus \beta$ of two uniform spaces $\alpha$ and $\beta$ is equal to the supremum of the pushforwards of the uniformity filters of $\alpha$ and $\beta$ under the left and right inclusion maps respectively. That is, \[ \mathfrak{U}(\alpha \oplus \beta) = \text{map}(\text{inl} \times \text{inl})(\mathfrak{U}(\alpha)) \sqcup \text{map}(\text{inr} \times \text{inr})(\mathfrak{U}(\beta)) \] where $\text{inl} : \alpha \to \alpha \oplus \beta$ and $\text{inr} : \beta \to \alpha \oplus \beta$ are the inclusion maps.

uniformContinuous_inl theorem

: UniformContinuous (Sum.inl : α → α ⊕ β)

Full source

lemma uniformContinuous_inl : UniformContinuous (Sum.inl : α → α ⊕ β) := le_sup_left

Uniform Continuity of Left Inclusion Map in Disjoint Union of Uniform Spaces

Informal description

The left inclusion map $\text{inl} \colon \alpha \to \alpha \oplus \beta$ between uniform spaces is uniformly continuous. That is, for every entourage $V$ in the uniformity of $\alpha \oplus \beta$, there exists an entourage $U$ in the uniformity of $\alpha$ such that for all $(x, y) \in U$, the pair $(\text{inl}(x), \text{inl}(y))$ belongs to $V$.

uniformContinuous_inr theorem

: UniformContinuous (Sum.inr : β → α ⊕ β)

Full source

lemma uniformContinuous_inr : UniformContinuous (Sum.inr : β → α ⊕ β) := le_sup_right

Uniform Continuity of Right Inclusion in Disjoint Union

Informal description

The right inclusion map $\text{inr} \colon \beta \to \alpha \oplus \beta$ is uniformly continuous, where $\alpha \oplus \beta$ is equipped with the disjoint union uniform space structure.

instIsCountablyGeneratedProdSumUniformity instance

[IsCountablyGenerated (𝓤 α)] [IsCountablyGenerated (𝓤 β)] : IsCountablyGenerated (𝓤 (α ⊕ β))

Full source

instance [IsCountablyGenerated (𝓤 α)] [IsCountablyGenerated (𝓤 β)] :
    IsCountablyGenerated (𝓤 (α ⊕ β)) := by
  rw [Sum.uniformity]
  infer_instance

Countable Generation of Uniformity in Disjoint Union of Uniform Spaces

Informal description

If the uniformity filters $\mathfrak{U}(\alpha)$ and $\mathfrak{U}(\beta)$ of two uniform spaces $\alpha$ and $\beta$ are countably generated, then the uniformity filter $\mathfrak{U}(\alpha \oplus \beta)$ of their disjoint union is also countably generated.

Uniform.tendsto_nhds_right theorem

{f : Filter β} {u : β → α} {a : α} : Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α)

Full source

theorem tendsto_nhds_right {f : Filter β} {u : β → α} {a : α} :
    TendstoTendsto u f (𝓝 a) ↔ Tendsto (fun x => (a, u x)) f (𝓤 α) := by
  rw [nhds_eq_comap_uniformity, tendsto_comap_iff]; rfl

Right Uniform Limit Characterization via Uniformity

Informal description

For a filter $f$ on a type $\beta$, a function $u : \beta \to \alpha$, and a point $a \in \alpha$, the function $u$ tends to $a$ along the filter $f$ (i.e., $\lim_{f} u = a$) if and only if the map $x \mapsto (a, u(x))$ tends to the uniformity $\mathfrak{U}(\alpha)$ along $f$.

Uniform.tendsto_nhds_left theorem

{f : Filter β} {u : β → α} {a : α} : Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)

Full source

theorem tendsto_nhds_left {f : Filter β} {u : β → α} {a : α} :
    TendstoTendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α) := by
  rw [nhds_eq_comap_uniformity', tendsto_comap_iff]; rfl

Left Uniform Limit Characterization via Uniformity

Informal description

For a filter $f$ on a type $\beta$, a function $u : \beta \to \alpha$ mapping into a uniform space $\alpha$, and a point $a \in \alpha$, the function $u$ converges to $a$ along $f$ (i.e., $\lim_{f} u = a$) if and only if the map $x \mapsto (u(x), a)$ converges to the uniformity $\mathfrak{U}(\alpha)$ along $f$.

Uniform.continuousAt_iff'_right theorem

[TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)

Full source

theorem continuousAt_iff'_right [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAtContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α) := by
  rw [ContinuousAt, tendsto_nhds_right]

Right Uniform Continuity Criterion at a Point

Informal description

Let $f : \beta \to \alpha$ be a function between topological spaces, and let $b \in \beta$. Then $f$ is continuous at $b$ if and only if the map $x \mapsto (f(b), f(x))$ converges to the uniformity $\mathfrak{U}(\alpha)$ as $x$ approaches $b$.

Uniform.continuousAt_iff'_left theorem

[TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)

Full source

theorem continuousAt_iff'_left [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAtContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α) := by
  rw [ContinuousAt, tendsto_nhds_left]

Left Uniform Continuity Criterion at a Point

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous at a point $b \in X$ if and only if the map $x \mapsto (f(x), f(b))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ in $X$.

Uniform.continuousAt_iff_prod theorem

 [TopologicalSpace β] {f : β → α} {b : β} :
  ContinuousAt f b ↔ Tendsto (fun x : β × β => (f x.1, f x.2)) (𝓝 (b, b)) (𝓤 α)

Full source

theorem continuousAt_iff_prod [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAtContinuousAt f b ↔ Tendsto (fun x : β × β => (f x.1, f x.2)) (𝓝 (b, b)) (𝓤 α) :=
  ⟨fun H => le_trans (H.prodMap' H) (nhds_le_uniformity _), fun H =>
    continuousAt_iff'_left.2 <| H.comp <| tendsto_id.prodMk_nhds tendsto_const_nhds⟩

Product Uniform Continuity Criterion at a Point

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous at a point $b \in X$ if and only if the map $(x_1, x_2) \mapsto (f(x_1), f(x_2))$ tends to the uniformity $\mathfrak{U}(Y)$ as $(x_1, x_2)$ approaches $(b, b)$ in $X \times X$.

Uniform.continuousWithinAt_iff'_right theorem

 [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
  ContinuousWithinAt f s b ↔ Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)

Full source

theorem continuousWithinAt_iff'_right [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAtContinuousWithinAt f s b ↔ Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α) := by
  rw [ContinuousWithinAt, tendsto_nhds_right]

Uniform Continuity at a Point within a Subset (Right Version)

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous at a point $b \in X$ within a subset $s \subseteq X$ if and only if the map $x \mapsto (f(b), f(x))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ within $s$.

Uniform.continuousWithinAt_iff'_left theorem

 [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
  ContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)

Full source

theorem continuousWithinAt_iff'_left [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAtContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α) := by
  rw [ContinuousWithinAt, tendsto_nhds_left]

Uniform Continuity at a Point within a Subset (Left Version)

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous at a point $b \in X$ within a subset $s \subseteq X$ if and only if the map $x \mapsto (f(x), f(b))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ within $s$.

Uniform.continuousOn_iff'_right theorem

 [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α)

Full source

theorem continuousOn_iff'_right [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOnContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f b, f x)) (𝓝[s] b) (𝓤 α) := by
  simp [ContinuousOn, continuousWithinAt_iff'_right]

Uniform Continuity Criterion on Subsets (Right Version)

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous on a subset $s \subseteq X$ if and only if for every point $b \in s$, the map $(f(b), f(\cdot))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ within $s$.

Uniform.continuousOn_iff'_left theorem

 [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)

Full source

theorem continuousOn_iff'_left [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOnContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α) := by
  simp [ContinuousOn, continuousWithinAt_iff'_left]

Uniform Continuity Criterion on Subsets (Left Version)

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous on a subset $s \subseteq X$ if and only if for every point $b \in s$, the map $(f(\cdot), f(b))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ within $s$.

Uniform.continuous_iff'_right theorem

[TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ b, Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)

Full source

theorem continuous_iff'_right [TopologicalSpace β] {f : β → α} :
    ContinuousContinuous f ↔ ∀ b, Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α) :=
  continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_right

Uniform Continuity Criterion (Right Version)

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous if and only if for every point $b \in X$, the map $(f(b), f(\cdot))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ in $X$.

Uniform.continuous_iff'_left theorem

[TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ b, Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)

Full source

theorem continuous_iff'_left [TopologicalSpace β] {f : β → α} :
    ContinuousContinuous f ↔ ∀ b, Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α) :=
  continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_left

Uniform Continuity Criterion (Left Version)

Informal description

Let $X$ be a topological space and $Y$ a uniform space. A function $f : X \to Y$ is continuous if and only if for every point $b \in X$, the map $(f(\cdot), f(b))$ tends to the uniformity $\mathfrak{U}(Y)$ as $x$ approaches $b$ in $X$.

Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq theorem

 [TopologicalSpace β] {r : Set (α × α)} {s : Set β} {f g : β → α} (hf : ∀ x ∈ s, ContinuousAt f x)
  (hg : ∀ x ∈ s, ContinuousAt g x) (hfg : s.EqOn f g) (hr : r ∈ 𝓤 α) : ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Full source

/-- Consider two functions `f` and `g` which coincide on a set `s` and are continuous there.
Then there is an open neighborhood of `s` on which `f` and `g` are uniformly close. -/
lemma exists_is_open_mem_uniformity_of_forall_mem_eq
    [TopologicalSpace β] {r : Set (α × α)} {s : Set β}
    {f g : β → α} (hf : ∀ x ∈ s, ContinuousAt f x) (hg : ∀ x ∈ s, ContinuousAt g x)
    (hfg : s.EqOn f g) (hr : r ∈ 𝓤 α) :
    ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r := by
  have A : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r := by
    intro x hx
    obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
    have A : {z | (f x, f z) ∈ t}{z | (f x, f z) ∈ t} ∈ 𝓝 x := (hf x hx).preimage_mem_nhds (mem_nhds_left (f x) ht)
    have B : {z | (g x, g z) ∈ t}{z | (g x, g z) ∈ t} ∈ 𝓝 x := (hg x hx).preimage_mem_nhds (mem_nhds_left (g x) ht)
    rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩
    refine ⟨u, u_open, xu, fun y hy ↦ ?_⟩
    have I1 : (f y, f x)(f y, f x) ∈ t := (htsymm.mk_mem_comm).2 (hu hy).1
    have I2 : (g x, g y)(g x, g y) ∈ t := (hu hy).2
    rw [hfg hx] at I1
    exact htr (prodMk_mem_compRel I1 I2)
  choose! t t_open xt ht using A
  refine ⟨⋃ x ∈ s, t x, isOpen_biUnion t_open, fun x hx ↦ mem_biUnion hx (xt x hx), ?_⟩
  rintro x hx
  simp only [mem_iUnion, exists_prop] at hx
  rcases hx with ⟨y, ys, hy⟩
  exact ht y ys x hy

Uniform Approximation of Coinciding Continuous Functions on Neighborhoods

Informal description

Let $\beta$ be a topological space and $\alpha$ a uniform space. Given two functions $f, g \colon \beta \to \alpha$ that are continuous at every point of a set $s \subseteq \beta$ and coincide on $s$, and given an entourage $r \in \mathfrak{U}(\alpha)$, there exists an open set $t \subseteq \beta$ containing $s$ such that $(f(x), g(x)) \in r$ for all $x \in t$.

Filter.Tendsto.congr_uniformity theorem

 {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hf : Tendsto f l (𝓝 b))
  (hg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) : Tendsto g l (𝓝 b)

Full source

theorem Filter.Tendsto.congr_uniformity {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β}
    (hf : Tendsto f l (𝓝 b)) (hg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) : Tendsto g l (𝓝 b) :=
  Uniform.tendsto_nhds_right.2 <| (Uniform.tendsto_nhds_right.1 hf).uniformity_trans hg

Uniform Limit Congruence via Uniformity

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform space structure. Given two functions $f, g : \alpha \to \beta$, a filter $l$ on $\alpha$, and a point $b \in \beta$, if $f$ tends to $b$ along $l$ (i.e., $\lim_{l} f = b$) and the pairs $(f(x), g(x))$ tend to the uniformity $\mathfrak{U}(\beta)$ along $l$, then $g$ also tends to $b$ along $l$.

Uniform.tendsto_congr theorem

 {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hfg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) :
  Tendsto f l (𝓝 b) ↔ Tendsto g l (𝓝 b)

Full source

theorem Uniform.tendsto_congr {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β}
    (hfg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) : TendstoTendsto f l (𝓝 b) ↔ Tendsto g l (𝓝 b) :=
  ⟨fun h => h.congr_uniformity hfg, fun h => h.congr_uniformity hfg.uniformity_symm⟩

Uniform Limit Criterion via Uniformity: $f \to b \iff g \to b$ when $(f, g) \to \mathfrak{U}(\beta)$

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a uniform space structure. Given two functions $f, g \colon \alpha \to \beta$, a filter $l$ on $\alpha$, and a point $b \in \beta$, if the pairs $(f(x), g(x))$ tend to the uniformity $\mathfrak{U}(\beta)$ along $l$, then $f$ tends to $b$ along $l$ if and only if $g$ tends to $b$ along $l$.

Mathlib.Topology.UniformSpace.Basic

Main definitions

Notations

References