Mathlib.Topology.UniformSpace.Equicontinuity

EquicontinuousAt definition

(F : ι → X → α) (x₀ : X) : Prop

Full source

/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous at `x₀ : X`* if, for all entourages `U ∈ 𝓤 α`, there is a neighborhood `V` of `x₀`
such that, for all `x ∈ V` and for all `i : ι`, `F i x` is `U`-close to `F i x₀`. -/
def EquicontinuousAt (F : ι → X → α) (x₀ : X) : Prop :=
  ∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ U

Equicontinuity at a point for a family of functions

Informal description

A family of functions $ F : \iota \to X \to \alpha $ from a topological space $ X $ to a uniform space $ \alpha $ is called *equicontinuous at a point $ x_0 \in X $* if, for every entourage $ U $ in the uniformity of $ \alpha $, there exists a neighborhood $ V $ of $ x_0 $ such that for all $ x \in V $ and all indices $ i \in \iota $, the pair $ (F_i x_0, F_i x) $ belongs to $ U $.

Set.EquicontinuousAt abbrev

(H : Set <| X → α) (x₀ : X) : Prop

Full source

/-- We say that a set `H : Set (X → α)` of functions is equicontinuous at a point if the family
`(↑) : ↥H → (X → α)` is equicontinuous at that point. -/
protected abbrev Set.EquicontinuousAt (H : Set <| X → α) (x₀ : X) : Prop :=
  EquicontinuousAt ((↑) : H → X → α) x₀

Equicontinuity at a Point for a Set of Functions

Informal description

A set $H$ of functions from a topological space $X$ to a uniform space $\alpha$ is called *equicontinuous at a point $x_0 \in X$* if the family of functions obtained by viewing $H$ as an indexed family (via the inclusion map) is equicontinuous at $x_0$. More precisely, for every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x \in V$ and all functions $f \in H$, the pair $(f(x_0), f(x))$ belongs to $U$.

EquicontinuousWithinAt definition

(F : ι → X → α) (S : Set X) (x₀ : X) : Prop

Full source

/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous at `x₀ : X` within `S : Set X`* if, for all entourages `U ∈ 𝓤 α`, there is a
neighborhood `V` of `x₀` within `S` such that, for all `x ∈ V` and for all `i : ι`, `F i x` is
`U`-close to `F i x₀`. -/
def EquicontinuousWithinAt (F : ι → X → α) (S : Set X) (x₀ : X) : Prop :=
  ∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ U

Equicontinuity at a point within a subset

Informal description

A family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is called *equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$* if, for every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ within $S$ such that for all $x \in V$ and all indices $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $U$. In other words, for any uniformity condition $U$, there's a neighborhood where all functions in the family simultaneously satisfy the $U$-closeness condition at $x_0$ within $S$.

Set.EquicontinuousWithinAt abbrev

(H : Set <| X → α) (S : Set X) (x₀ : X) : Prop

Full source

/-- We say that a set `H : Set (X → α)` of functions is equicontinuous at a point within a subset
if the family `(↑) : ↥H → (X → α)` is equicontinuous at that point within that same subset. -/
protected abbrev Set.EquicontinuousWithinAt (H : Set <| X → α) (S : Set X) (x₀ : X) : Prop :=
  EquicontinuousWithinAt ((↑) : H → X → α) S x₀

Equicontinuity of a Function Set at a Point Within a Subset

Informal description

A set of functions $H \subseteq (X \to \alpha)$ from a topological space $X$ to a uniform space $\alpha$ is called *equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$* if, for every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ within $S$ such that for all $x \in V$ and all functions $f \in H$, the pair $(f(x_0), f(x))$ belongs to $U$.

Equicontinuous definition

(F : ι → X → α) : Prop

Full source

/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous* on all of `X` if it is equicontinuous at each point of `X`. -/
def Equicontinuous (F : ι → X → α) : Prop :=
  ∀ x₀, EquicontinuousAt F x₀

Equicontinuity of a family of functions

Informal description

A family of functions $ F : \iota \to X \to \alpha $ from a topological space $ X $ to a uniform space $ \alpha $ is called *equicontinuous* if it is equicontinuous at every point $ x_0 \in X $. That is, for every $ x_0 \in X $ and every entourage $ U $ in the uniformity of $ \alpha $, there exists a neighborhood $ V $ of $ x_0 $ such that for all $ x \in V $ and all $ i \in \iota $, the pair $ (F_i x_0, F_i x) $ belongs to $ U $.

Set.Equicontinuous abbrev

(H : Set <| X → α) : Prop

Full source

/-- We say that a set `H : Set (X → α)` of functions is equicontinuous if the family
`(↑) : ↥H → (X → α)` is equicontinuous. -/
protected abbrev Set.Equicontinuous (H : Set <| X → α) : Prop :=
  Equicontinuous ((↑) : H → X → α)

Equicontinuity of a Function Set

Informal description

A set of functions $H \subseteq (X \to \alpha)$ from a topological space $X$ to a uniform space $\alpha$ is called *equicontinuous* if the family of functions obtained by considering $H$ as an indexed family (via the inclusion map) is equicontinuous. That is, for every point $x_0 \in X$ and every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x \in V$ and all $f \in H$, the pair $(f(x_0), f(x))$ belongs to $U$.

EquicontinuousOn definition

(F : ι → X → α) (S : Set X) : Prop

Full source

/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous on `S : Set X`* if it is equicontinuous *within `S`* at each point of `S`. -/
def EquicontinuousOn (F : ι → X → α) (S : Set X) : Prop :=
  ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀

Equicontinuity on a subset

Informal description

A family of functions $ F : \iota \to X \to \alpha $ from a topological space $ X $ to a uniform space $ \alpha $ is called *equicontinuous on a subset $ S \subseteq X $* if, for every point $ x_0 \in S $, the family $ F $ is equicontinuous at $ x_0 $ within $ S $. This means that for every entourage $ U $ in the uniformity of $ \alpha $ and every $ x_0 \in S $, there exists a neighborhood $ V $ of $ x_0 $ within $ S $ such that for all $ x \in V $ and all indices $ i \in \iota $, the pair $ (F_i x_0, F_i x) $ belongs to $ U $.

Set.EquicontinuousOn abbrev

(H : Set <| X → α) (S : Set X) : Prop

Full source

/-- We say that a set `H : Set (X → α)` of functions is equicontinuous on a subset if the family
`(↑) : ↥H → (X → α)` is equicontinuous on that subset. -/
protected abbrev Set.EquicontinuousOn (H : Set <| X → α) (S : Set X) : Prop :=
  EquicontinuousOn ((↑) : H → X → α) S

Equicontinuity of a Function Set on a Subset

Informal description

A set of functions $H \subseteq (X \to \alpha)$ from a topological space $X$ to a uniform space $\alpha$ is called *equicontinuous on a subset $S \subseteq X$* if, for every point $x_0 \in S$ and every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ within $S$ such that for all $x \in V$ and all $f \in H$, the pair $(f(x_0), f(x))$ belongs to $U$.

UniformEquicontinuous definition

(F : ι → β → α) : Prop

Full source

/-- A family `F : ι → β → α` of functions between uniform spaces is *uniformly equicontinuous* if,
for all entourages `U ∈ 𝓤 α`, there is an entourage `V ∈ 𝓤 β` such that, whenever `x` and `y` are
`V`-close, we have that, *for all `i : ι`*, `F i x` is `U`-close to `F i y`. -/
def UniformEquicontinuous (F : ι → β → α) : Prop :=
  ∀ U ∈ 𝓤 α, ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ U

Uniformly equicontinuous family of functions

Informal description

A family of functions $ F : \iota \to \beta \to \alpha $ between uniform spaces is *uniformly equicontinuous* if, for every entourage $ U $ in the uniformity of $ \alpha $, there exists an entourage $ V $ in the uniformity of $ \beta $ such that for all $ (x, y) \in V $ and for all $ i \in \iota $, the pair $ (F_i x, F_i y) $ belongs to $ U $.

Set.UniformEquicontinuous abbrev

(H : Set <| β → α) : Prop

Full source

/-- We say that a set `H : Set (X → α)` of functions is uniformly equicontinuous if the family
`(↑) : ↥H → (X → α)` is uniformly equicontinuous. -/
protected abbrev Set.UniformEquicontinuous (H : Set <| β → α) : Prop :=
  UniformEquicontinuous ((↑) : H → β → α)

Uniform Equicontinuity of a Set of Functions

Informal description

A set $H$ of functions from a uniform space $\beta$ to a uniform space $\alpha$ is *uniformly equicontinuous* if, for every entourage $U$ in the uniformity of $\alpha$, there exists an entourage $V$ in the uniformity of $\beta$ such that for all $(x, y) \in V$ and for all $f \in H$, the pair $(f(x), f(y))$ belongs to $U$.

UniformEquicontinuousOn definition

(F : ι → β → α) (S : Set β) : Prop

Full source

/-- A family `F : ι → β → α` of functions between uniform spaces is
*uniformly equicontinuous on `S : Set β`* if, for all entourages `U ∈ 𝓤 α`, there is a relative
entourage `V ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)` such that, whenever `x` and `y` are `V`-close, we have that,
*for all `i : ι`*, `F i x` is `U`-close to `F i y`. -/
def UniformEquicontinuousOn (F : ι → β → α) (S : Set β) : Prop :=
  ∀ U ∈ 𝓤 α, ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ U

Uniform equicontinuity on a subset

Informal description

A family of functions $ F : \iota \to \beta \to \alpha $ between uniform spaces is *uniformly equicontinuous on a subset $ S \subseteq \beta $* if, for every entourage $ U $ in the uniformity of $ \alpha $, there exists a relative entourage $ V $ in the uniformity of $ \beta $ restricted to $ S \times S $ such that for all $ (x, y) \in V $ and for all $ i \in \iota $, the pair $ (F_i x, F_i y) $ belongs to $ U $.

Set.UniformEquicontinuousOn abbrev

(H : Set <| β → α) (S : Set β) : Prop

Full source

/-- We say that a set `H : Set (X → α)` of functions is uniformly equicontinuous on a subset if the
family `(↑) : ↥H → (X → α)` is uniformly equicontinuous on that subset. -/
protected abbrev Set.UniformEquicontinuousOn (H : Set <| β → α) (S : Set β) : Prop :=
  UniformEquicontinuousOn ((↑) : H → β → α) S

Uniform Equicontinuity of a Set of Functions on a Subset

Informal description

A set $H$ of functions from a uniform space $\beta$ to a uniform space $\alpha$ is *uniformly equicontinuous on a subset $S \subseteq \beta$* if, for every entourage $U$ in the uniformity of $\alpha$, there exists an entourage $V$ in the uniformity of $\beta$ such that for all $(x, y) \in V \cap (S \times S)$ and for all $f \in H$, the pair $(f(x), f(y))$ belongs to $U$.

EquicontinuousAt.equicontinuousWithinAt theorem

{F : ι → X → α} {x₀ : X} (H : EquicontinuousAt F x₀) (S : Set X) : EquicontinuousWithinAt F S x₀

Full source

lemma EquicontinuousAt.equicontinuousWithinAt {F : ι → X → α} {x₀ : X} (H : EquicontinuousAt F x₀)
    (S : Set X) : EquicontinuousWithinAt F S x₀ :=
  fun U hU ↦ (H U hU).filter_mono inf_le_left

Equicontinuity at a point implies equicontinuity within any subset

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a family of functions $F : \iota \to X \to \alpha$ that is equicontinuous at a point $x_0 \in X$, then for any subset $S \subseteq X$, the family $F$ is equicontinuous at $x_0$ within $S$.

EquicontinuousWithinAt.mono theorem

 {F : ι → X → α} {x₀ : X} {S T : Set X} (H : EquicontinuousWithinAt F T x₀) (hST : S ⊆ T) :
  EquicontinuousWithinAt F S x₀

Full source

lemma EquicontinuousWithinAt.mono {F : ι → X → α} {x₀ : X} {S T : Set X}
    (H : EquicontinuousWithinAt F T x₀) (hST : S ⊆ T) : EquicontinuousWithinAt F S x₀ :=
  fun U hU ↦ (H U hU).filter_mono <| nhdsWithin_mono x₀ hST

Restriction of Equicontinuity to Smaller Subsets

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Let $F : \iota \to X \to \alpha$ be a family of functions, $x_0 \in X$ a point, and $S, T \subseteq X$ subsets with $S \subseteq T$. If $F$ is equicontinuous at $x_0$ within $T$, then $F$ is equicontinuous at $x_0$ within $S$. In other words, equicontinuity within a larger set implies equicontinuity within any smaller subset.

equicontinuousWithinAt_univ theorem

(F : ι → X → α) (x₀ : X) : EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀

Full source

@[simp] lemma equicontinuousWithinAt_univ (F : ι → X → α) (x₀ : X) :
    EquicontinuousWithinAtEquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀ := by
  rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]

Equivalence of Equicontinuity within Entire Space and Pointwise Equicontinuity

Informal description

For a family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, and a point $x_0 \in X$, the following are equivalent: 1. The family $F$ is equicontinuous at $x_0$ within the entire space $X$. 2. The family $F$ is equicontinuous at $x_0$. Here, equicontinuity at $x_0$ means that for every entourage $U$ in $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x \in V$ and all $i \in \iota$, the pair $(F_i x_0, F_i x)$ is in $U$.

equicontinuousAt_restrict_iff theorem

 (F : ι → X → α) {S : Set X} (x₀ : S) : EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S x₀

Full source

lemma equicontinuousAt_restrict_iff (F : ι → X → α) {S : Set X} (x₀ : S) :
    EquicontinuousAtEquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S x₀ := by
  simp [EquicontinuousWithinAt, EquicontinuousAt,
    ← eventually_nhds_subtype_iff]

Equivalence of Equicontinuity for Restricted and Original Families at a Point

Informal description

For a family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, and a subset $S \subseteq X$ with a point $x_0 \in S$, the following are equivalent: 1. The restricted family $(S.\text{restrict} \circ F) : \iota \to S \to \alpha$ is equicontinuous at $x_0$. 2. The original family $F$ is equicontinuous at $x_0$ within $S$. Here, equicontinuity at $x_0$ means that for every entourage $U$ in $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x \in V$ and all $i \in \iota$, the pair $(F_i x_0, F_i x)$ is in $U$. The restricted family uses the subspace topology on $S$.

Equicontinuous.equicontinuousOn theorem

{F : ι → X → α} (H : Equicontinuous F) (S : Set X) : EquicontinuousOn F S

Full source

lemma Equicontinuous.equicontinuousOn {F : ι → X → α} (H : Equicontinuous F)
    (S : Set X) : EquicontinuousOn F S :=
  fun x _ ↦ (H x).equicontinuousWithinAt S

Equicontinuity implies equicontinuity on any subset

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. If a family of functions $F : \iota \to X \to \alpha$ is equicontinuous (i.e., equicontinuous at every point of $X$), then for any subset $S \subseteq X$, the family $F$ is equicontinuous on $S$.

EquicontinuousOn.mono theorem

{F : ι → X → α} {S T : Set X} (H : EquicontinuousOn F T) (hST : S ⊆ T) : EquicontinuousOn F S

Full source

lemma EquicontinuousOn.mono {F : ι → X → α} {S T : Set X}
    (H : EquicontinuousOn F T) (hST : S ⊆ T) : EquicontinuousOn F S :=
  fun x hx ↦ (H x (hST hx)).mono hST

Restriction of Equicontinuity to Smaller Subsets

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a family of functions $F : \iota \to X \to \alpha$ and subsets $S, T \subseteq X$ with $S \subseteq T$, if $F$ is equicontinuous on $T$, then $F$ is equicontinuous on $S$.

equicontinuousOn_univ theorem

(F : ι → X → α) : EquicontinuousOn F univ ↔ Equicontinuous F

Full source

lemma equicontinuousOn_univ (F : ι → X → α) :
    EquicontinuousOnEquicontinuousOn F univ ↔ Equicontinuous F := by
  simp [EquicontinuousOn, Equicontinuous]

Equicontinuity on Universal Set vs. Global Equicontinuity

Informal description

For a family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, the following are equivalent: 1. The family $F$ is equicontinuous on the entire space $X$ (i.e., equicontinuous at every point of $X$). 2. The family $F$ is equicontinuous on the universal subset $\text{univ} = X$.

equicontinuous_restrict_iff theorem

(F : ι → X → α) {S : Set X} : Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S

Full source

lemma equicontinuous_restrict_iff (F : ι → X → α) {S : Set X} :
    EquicontinuousEquicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S := by
  simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff]

Equicontinuity of Restricted Family vs. Equicontinuity on Subset

Informal description

For a family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, and a subset $S \subseteq X$, the following are equivalent: 1. The family obtained by restricting each $F_i$ to $S$ (denoted $S.restrict \circ F$) is equicontinuous on $X$. 2. The original family $F$ is equicontinuous on $S$. In other words, the equicontinuity of the restricted family is equivalent to the equicontinuity of the original family when considered only on the subset $S$.

UniformEquicontinuous.uniformEquicontinuousOn theorem

{F : ι → β → α} (H : UniformEquicontinuous F) (S : Set β) : UniformEquicontinuousOn F S

Full source

lemma UniformEquicontinuous.uniformEquicontinuousOn {F : ι → β → α} (H : UniformEquicontinuous F)
    (S : Set β) : UniformEquicontinuousOn F S :=
  fun U hU ↦ (H U hU).filter_mono inf_le_left

Uniform equicontinuity implies uniform equicontinuity on subsets

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces. If $F$ is uniformly equicontinuous, then for any subset $S \subseteq \beta$, the family $F$ is uniformly equicontinuous on $S$.

UniformEquicontinuousOn.mono theorem

{F : ι → β → α} {S T : Set β} (H : UniformEquicontinuousOn F T) (hST : S ⊆ T) : UniformEquicontinuousOn F S

Full source

lemma UniformEquicontinuousOn.mono {F : ι → β → α} {S T : Set β}
    (H : UniformEquicontinuousOn F T) (hST : S ⊆ T) : UniformEquicontinuousOn F S :=
  fun U hU ↦ (H U hU).filter_mono <| by gcongr

Uniform Equicontinuity on Subset via Superset

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces, and let $S, T \subseteq \beta$ with $S \subseteq T$. If $F$ is uniformly equicontinuous on $T$, then $F$ is uniformly equicontinuous on $S$.

uniformEquicontinuousOn_univ theorem

(F : ι → β → α) : UniformEquicontinuousOn F univ ↔ UniformEquicontinuous F

Full source

lemma uniformEquicontinuousOn_univ (F : ι → β → α) :
    UniformEquicontinuousOnUniformEquicontinuousOn F univ ↔ UniformEquicontinuous F := by
  simp [UniformEquicontinuousOn, UniformEquicontinuous]

Uniform Equicontinuity on the Whole Space vs. Uniform Equicontinuity

Informal description

For a family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces, $F$ is uniformly equicontinuous on the entire space $\beta$ if and only if it is uniformly equicontinuous.

uniformEquicontinuous_restrict_iff theorem

(F : ι → β → α) {S : Set β} : UniformEquicontinuous (S.restrict ∘ F) ↔ UniformEquicontinuousOn F S

Full source

lemma uniformEquicontinuous_restrict_iff (F : ι → β → α) {S : Set β} :
    UniformEquicontinuousUniformEquicontinuous (S.restrict ∘ F) ↔ UniformEquicontinuousOn F S := by
  rw [UniformEquicontinuous, UniformEquicontinuousOn]
  conv in _ ⊓ _ => rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]
  rfl

Uniform Equicontinuity of Restricted Family vs. Uniform Equicontinuity on Subset

Informal description

For a family of functions $ F : \iota \to \beta \to \alpha $ between uniform spaces and a subset $ S \subseteq \beta $, the family $ F $ is uniformly equicontinuous on $ S $ if and only if the restricted family $ S.restrict \circ F $ is uniformly equicontinuous on the entire space $ \beta $.

equicontinuousAt_empty theorem

[h : IsEmpty ι] (F : ι → X → α) (x₀ : X) : EquicontinuousAt F x₀

Full source

@[simp]
lemma equicontinuousAt_empty [h : IsEmpty ι] (F : ι → X → α) (x₀ : X) :
    EquicontinuousAt F x₀ :=
  fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Equicontinuity at a Point for Empty Family of Functions

Informal description

For any empty index type $\iota$ (i.e., $\iota$ has no elements), any family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, and any point $x_0 \in X$, the family $F$ is equicontinuous at $x_0$.

equicontinuousWithinAt_empty theorem

[h : IsEmpty ι] (F : ι → X → α) (S : Set X) (x₀ : X) : EquicontinuousWithinAt F S x₀

Full source

@[simp]
lemma equicontinuousWithinAt_empty [h : IsEmpty ι] (F : ι → X → α) (S : Set X) (x₀ : X) :
    EquicontinuousWithinAt F S x₀ :=
  fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Equicontinuity Within a Subset for Empty Family of Functions

Informal description

For any empty index type $\iota$, any family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, any subset $S \subseteq X$, and any point $x_0 \in X$, the family $F$ is equicontinuous at $x_0$ within $S$.

equicontinuous_empty theorem

[IsEmpty ι] (F : ι → X → α) : Equicontinuous F

Full source

@[simp]
lemma equicontinuous_empty [IsEmpty ι] (F : ι → X → α) :
    Equicontinuous F :=
  equicontinuousAt_empty F

Equicontinuity of the Empty Family of Functions

Informal description

For any empty index type $\iota$ and any family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, the family $F$ is equicontinuous (i.e., equicontinuous at every point of $X$).

equicontinuousOn_empty theorem

[IsEmpty ι] (F : ι → X → α) (S : Set X) : EquicontinuousOn F S

Full source

@[simp]
lemma equicontinuousOn_empty [IsEmpty ι] (F : ι → X → α) (S : Set X) :
    EquicontinuousOn F S :=
  fun x₀ _ ↦ equicontinuousWithinAt_empty F S x₀

Equicontinuity on Subset for Empty Family of Functions

Informal description

For any empty index type $\iota$, any family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, and any subset $S \subseteq X$, the family $F$ is equicontinuous on $S$.

uniformEquicontinuous_empty theorem

[h : IsEmpty ι] (F : ι → β → α) : UniformEquicontinuous F

Full source

@[simp]
lemma uniformEquicontinuous_empty [h : IsEmpty ι] (F : ι → β → α) :
    UniformEquicontinuous F :=
  fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Uniform Equicontinuity for Empty Index Families

Informal description

For any empty index type $\iota$ and any family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces, the family $F$ is uniformly equicontinuous.

uniformEquicontinuousOn_empty theorem

[h : IsEmpty ι] (F : ι → β → α) (S : Set β) : UniformEquicontinuousOn F S

Full source

@[simp]
lemma uniformEquicontinuousOn_empty [h : IsEmpty ι] (F : ι → β → α) (S : Set β) :
    UniformEquicontinuousOn F S :=
  fun _ _ ↦ Eventually.of_forall (fun _ ↦ h.elim)

Uniform Equicontinuity on a Subset for Empty Index Families

Informal description

For any empty index type $\iota$, any family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces, and any subset $S \subseteq \beta$, the family $F$ is uniformly equicontinuous on $S$.

equicontinuousAt_finite theorem

[Finite ι] {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ∀ i, ContinuousAt (F i) x₀

Full source

theorem equicontinuousAt_finite [Finite ι] {F : ι → X → α} {x₀ : X} :
    EquicontinuousAtEquicontinuousAt F x₀ ↔ ∀ i, ContinuousAt (F i) x₀ := by
  simp [EquicontinuousAt, ContinuousAt, (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff,
    UniformSpace.ball, @forall_swap _ ι]

Equicontinuity at a Point for Finite Families of Functions

Informal description

For a finite index set $\iota$, a family of functions $F : \iota \to X \to \alpha$ is equicontinuous at a point $x_0 \in X$ if and only if each function $F_i$ is continuous at $x_0$ for every $i \in \iota$.

equicontinuousWithinAt_finite theorem

 [Finite ι] {F : ι → X → α} {S : Set X} {x₀ : X} : EquicontinuousWithinAt F S x₀ ↔ ∀ i, ContinuousWithinAt (F i) S x₀

Full source

theorem equicontinuousWithinAt_finite [Finite ι] {F : ι → X → α} {S : Set X} {x₀ : X} :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔ ∀ i, ContinuousWithinAt (F i) S x₀ := by
  simp [EquicontinuousWithinAt, ContinuousWithinAt,
    (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball,
    @forall_swap _ ι]

Equicontinuity Within a Subset for Finite Families is Equivalent to Pointwise Continuity

Informal description

For a finite index set $\iota$, a family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$ if and only if each function $F_i$ is continuous at $x_0$ within $S$ for every $i \in \iota$.

equicontinuous_finite theorem

[Finite ι] {F : ι → X → α} : Equicontinuous F ↔ ∀ i, Continuous (F i)

Full source

theorem equicontinuous_finite [Finite ι] {F : ι → X → α} :
    EquicontinuousEquicontinuous F ↔ ∀ i, Continuous (F i) := by
  simp only [Equicontinuous, equicontinuousAt_finite, continuous_iff_continuousAt, @forall_swap ι]

Equicontinuity of Finite Families is Equivalent to Pointwise Continuity

Informal description

For a finite index set $\iota$ and a family of functions $F \colon \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, the family $F$ is equicontinuous if and only if each function $F_i$ is continuous for every $i \in \iota$.

equicontinuousOn_finite theorem

[Finite ι] {F : ι → X → α} {S : Set X} : EquicontinuousOn F S ↔ ∀ i, ContinuousOn (F i) S

Full source

theorem equicontinuousOn_finite [Finite ι] {F : ι → X → α} {S : Set X} :
    EquicontinuousOnEquicontinuousOn F S ↔ ∀ i, ContinuousOn (F i) S := by
  simp only [EquicontinuousOn, equicontinuousWithinAt_finite, ContinuousOn, @forall_swap ι]

Equicontinuity on a Subset for Finite Families is Equivalent to Pointwise Continuity on the Subset

Informal description

For a finite index type $\iota$, a family of functions $F \colon \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is equicontinuous on a subset $S \subseteq X$ if and only if each function $F_i$ is continuous on $S$ for every $i \in \iota$.

uniformEquicontinuous_finite theorem

[Finite ι] {F : ι → β → α} : UniformEquicontinuous F ↔ ∀ i, UniformContinuous (F i)

Full source

theorem uniformEquicontinuous_finite [Finite ι] {F : ι → β → α} :
    UniformEquicontinuousUniformEquicontinuous F ↔ ∀ i, UniformContinuous (F i) := by
  simp only [UniformEquicontinuous, eventually_all, @forall_swap _ ι]; rfl

Uniform Equicontinuity of Finite Families is Equivalent to Uniform Continuity of Each Member

Informal description

For a finite index type $\iota$ and a family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces, the family $F$ is uniformly equicontinuous if and only if each function $F_i$ is uniformly continuous for every $i \in \iota$.

uniformEquicontinuousOn_finite theorem

[Finite ι] {F : ι → β → α} {S : Set β} : UniformEquicontinuousOn F S ↔ ∀ i, UniformContinuousOn (F i) S

Full source

theorem uniformEquicontinuousOn_finite [Finite ι] {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔ ∀ i, UniformContinuousOn (F i) S := by
  simp only [UniformEquicontinuousOn, eventually_all, @forall_swap _ ι]; rfl

Uniform Equicontinuity on Subset for Finite Families is Equivalent to Uniform Continuity of Each Member on Subset

Informal description

For a finite index set $\iota$ and a family of functions $F \colon \iota \to \beta \to \alpha$ between uniform spaces, the family $F$ is uniformly equicontinuous on a subset $S \subseteq \beta$ if and only if for each $i \in \iota$, the function $F_i$ is uniformly continuous on $S$.

equicontinuousAt_unique theorem

[Unique ι] {F : ι → X → α} {x : X} : EquicontinuousAt F x ↔ ContinuousAt (F default) x

Full source

theorem equicontinuousAt_unique [Unique ι] {F : ι → X → α} {x : X} :
    EquicontinuousAtEquicontinuousAt F x ↔ ContinuousAt (F default) x :=
  equicontinuousAt_finite.trans Unique.forall_iff

Equicontinuity at a Point for Singleton Families is Equivalent to Continuity of the Default Function at the Point

Informal description

For a family of functions $F \colon \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, where the index type $\iota$ has a unique element, the family $F$ is equicontinuous at a point $x \in X$ if and only if the function $F(\text{default})$ is continuous at $x$.

equicontinuousWithinAt_unique theorem

 [Unique ι] {F : ι → X → α} {S : Set X} {x : X} : EquicontinuousWithinAt F S x ↔ ContinuousWithinAt (F default) S x

Full source

theorem equicontinuousWithinAt_unique [Unique ι] {F : ι → X → α} {S : Set X} {x : X} :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x ↔ ContinuousWithinAt (F default) S x :=
  equicontinuousWithinAt_finite.trans Unique.forall_iff

Equicontinuity Within Subset for Singleton Family is Equivalent to Continuity of Default Function Within Subset

Informal description

For a family of functions $F \colon \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, where the index type $\iota$ has a unique element, the family $F$ is equicontinuous at a point $x \in X$ within a subset $S \subseteq X$ if and only if the function $F(\text{default})$ is continuous at $x$ within $S$.

equicontinuous_unique theorem

[Unique ι] {F : ι → X → α} : Equicontinuous F ↔ Continuous (F default)

Full source

theorem equicontinuous_unique [Unique ι] {F : ι → X → α} :
    EquicontinuousEquicontinuous F ↔ Continuous (F default) :=
  equicontinuous_finite.trans Unique.forall_iff

Equicontinuity of Singleton Family is Equivalent to Continuity of Default Function

Informal description

For a family of functions $F \colon \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, where the index type $\iota$ has a unique element, the family $F$ is equicontinuous if and only if the function $F(\text{default})$ is continuous.

equicontinuousOn_unique theorem

[Unique ι] {F : ι → X → α} {S : Set X} : EquicontinuousOn F S ↔ ContinuousOn (F default) S

Full source

theorem equicontinuousOn_unique [Unique ι] {F : ι → X → α} {S : Set X} :
    EquicontinuousOnEquicontinuousOn F S ↔ ContinuousOn (F default) S :=
  equicontinuousOn_finite.trans Unique.forall_iff

Equicontinuity on Subset for Singleton Families is Equivalent to Continuity of the Default Function on Subset

Informal description

For a family of functions $F \colon \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$, where the index type $\iota$ has a unique element, the family $F$ is equicontinuous on a subset $S \subseteq X$ if and only if the function $F(\text{default})$ is continuous on $S$.

uniformEquicontinuous_unique theorem

[Unique ι] {F : ι → β → α} : UniformEquicontinuous F ↔ UniformContinuous (F default)

Full source

theorem uniformEquicontinuous_unique [Unique ι] {F : ι → β → α} :
    UniformEquicontinuousUniformEquicontinuous F ↔ UniformContinuous (F default) :=
  uniformEquicontinuous_finite.trans Unique.forall_iff

Uniform Equicontinuity of Singleton Family is Equivalent to Uniform Continuity of Default Function

Informal description

For a family of functions $F \colon \iota \to \beta \to \alpha$ between uniform spaces, where the index type $\iota$ has a unique element, the family $F$ is uniformly equicontinuous if and only if the function $F(\text{default})$ is uniformly continuous.

uniformEquicontinuousOn_unique theorem

[Unique ι] {F : ι → β → α} {S : Set β} : UniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S

Full source

theorem uniformEquicontinuousOn_unique [Unique ι] {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S :=
  uniformEquicontinuousOn_finite.trans Unique.forall_iff

Uniform Equicontinuity on Subset for Singleton Families is Equivalent to Uniform Continuity of the Default Function on Subset

Informal description

For a family of functions $F \colon \iota \to \beta \to \alpha$ between uniform spaces, where the index type $\iota$ has a unique element, the family $F$ is uniformly equicontinuous on a subset $S \subseteq \beta$ if and only if the function $F(\text{default})$ is uniformly continuous on $S$.

equicontinuousWithinAt_iff_pair theorem

 {F : ι → X → α} {S : Set X} {x₀ : X} (hx₀ : x₀ ∈ S) :
  EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U

Full source

/-- Reformulation of equicontinuity at `x₀` within a set `S`, comparing two variables near `x₀`
instead of comparing only one with `x₀`. -/
theorem equicontinuousWithinAt_iff_pair {F : ι → X → α} {S : Set X} {x₀ : X} (hx₀ : x₀ ∈ S) :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔
      ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U := by
  constructor <;> intro H U hU
  · rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
    refine ⟨_, H V hV, fun x hx y hy i => hVU (prodMk_mem_compRel ?_ (hy i))⟩
    exact hVsymm.mk_mem_comm.mp (hx i)
  · rcases H U hU with ⟨V, hV, hVU⟩
    filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i

Characterization of Equicontinuity at a Point within a Subset via Pairwise Uniform Closeness

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $S \subseteq X$ a subset, and $x_0 \in S$. A family of functions $F = (F_i)_{i \in \iota} \colon X \to \alpha$ is equicontinuous at $x_0$ within $S$ if and only if for every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ in $S$ such that for all $x, y \in V$ and all $i \in \iota$, the pair $(F_i(x), F_i(y))$ belongs to $U$.

equicontinuousAt_iff_pair theorem

 {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U

Full source

/-- Reformulation of equicontinuity at `x₀` comparing two variables near `x₀` instead of comparing
only one with `x₀`. -/
theorem equicontinuousAt_iff_pair {F : ι → X → α} {x₀ : X} :
    EquicontinuousAtEquicontinuousAt F x₀ ↔
      ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U := by
  simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀),
    nhdsWithin_univ]

Characterization of Equicontinuity at a Point via Pairwise Uniform Closeness

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, and $x_0 \in X$. A family of functions $F = (F_i)_{i \in \iota} \colon X \to \alpha$ is equicontinuous at $x_0$ if and only if for every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x, y \in V$ and all $i \in \iota$, the pair $(F_i(x), F_i(y))$ belongs to $U$.

UniformEquicontinuous.equicontinuous theorem

{F : ι → β → α} (h : UniformEquicontinuous F) : Equicontinuous F

Full source

/-- Uniform equicontinuity implies equicontinuity. -/
theorem UniformEquicontinuous.equicontinuous {F : ι → β → α} (h : UniformEquicontinuous F) :
    Equicontinuous F := fun x₀ U hU ↦
  mem_of_superset (ball_mem_nhds x₀ (h U hU)) fun _ hx i ↦ hx i

Uniform Equicontinuity Implies Pointwise Equicontinuity

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces. If $F$ is uniformly equicontinuous, then it is equicontinuous. That is, for every $x_0 \in \beta$ and every entourage $U$ in the uniformity of $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x \in V$ and all $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $U$.

UniformEquicontinuousOn.equicontinuousOn theorem

{F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S) : EquicontinuousOn F S

Full source

/-- Uniform equicontinuity on a subset implies equicontinuity on that subset. -/
theorem UniformEquicontinuousOn.equicontinuousOn {F : ι → β → α} {S : Set β}
    (h : UniformEquicontinuousOn F S) :
    EquicontinuousOn F S := fun _ hx₀ U hU ↦
  mem_of_superset (ball_mem_nhdsWithin hx₀ (h U hU)) fun _ hx i ↦ hx i

Uniform Equicontinuity on a Subset Implies Pointwise Equicontinuity on that Subset

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces, and let $S \subseteq \beta$. If $F$ is uniformly equicontinuous on $S$, then $F$ is equicontinuous on $S$. In other words, if for every entourage $U$ in the uniformity of $\alpha$ there exists an entourage $V$ in the uniformity of $\beta$ restricted to $S \times S$ such that for all $(x,y) \in V$ and all $i \in \iota$, we have $(F_i x, F_i y) \in U$, then for every $x_0 \in S$ and every entourage $U$ in $\alpha$, there exists a neighborhood $W$ of $x_0$ in $S$ such that for all $x \in W$ and all $i \in \iota$, we have $(F_i x_0, F_i x) \in U$.

EquicontinuousAt.continuousAt theorem

{F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (i : ι) : ContinuousAt (F i) x₀

Full source

/-- Each function of a family equicontinuous at `x₀` is continuous at `x₀`. -/
theorem EquicontinuousAt.continuousAt {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (i : ι) :
    ContinuousAt (F i) x₀ :=
  (UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i

Continuity of Functions in an Equicontinuous Family at a Point

Informal description

Let $ X $ be a topological space and $ \alpha $ a uniform space. Given a family of functions $ F : \iota \to X \to \alpha $ that is equicontinuous at a point $ x_0 \in X $, then for any index $ i \in \iota $, the function $ F_i $ is continuous at $ x_0 $.

EquicontinuousWithinAt.continuousWithinAt theorem

 {F : ι → X → α} {S : Set X} {x₀ : X} (h : EquicontinuousWithinAt F S x₀) (i : ι) : ContinuousWithinAt (F i) S x₀

Full source

/-- Each function of a family equicontinuous at `x₀` within `S` is continuous at `x₀` within `S`. -/
theorem EquicontinuousWithinAt.continuousWithinAt {F : ι → X → α} {S : Set X} {x₀ : X}
    (h : EquicontinuousWithinAt F S x₀) (i : ι) :
    ContinuousWithinAt (F i) S x₀ :=
  (UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i

Equicontinuity within a subset implies continuity within the subset

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a family of functions $F : \iota \to X \to \alpha$ that is equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$, then for every index $i \in \iota$, the function $F_i$ is continuous at $x_0$ within $S$. In other words, if for every entourage $U$ in $\alpha$ there exists a neighborhood $V$ of $x_0$ in $S$ such that for all $x \in V$ and all $i \in \iota$, $(F_i x_0, F_i x) \in U$, then each individual function $F_i$ is continuous at $x_0$ within $S$.

Set.EquicontinuousAt.continuousAt_of_mem theorem

{H : Set <| X → α} {x₀ : X} (h : H.EquicontinuousAt x₀) {f : X → α} (hf : f ∈ H) : ContinuousAt f x₀

Full source

protected theorem Set.EquicontinuousAt.continuousAt_of_mem {H : Set <| X → α} {x₀ : X}
    (h : H.EquicontinuousAt x₀) {f : X → α} (hf : f ∈ H) : ContinuousAt f x₀ :=
  h.continuousAt ⟨f, hf⟩

Continuity of Functions in an Equicontinuous Set at a Point

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a set $H$ of functions from $X$ to $\alpha$ that is equicontinuous at a point $x_0 \in X$, then any function $f \in H$ is continuous at $x_0$.

Set.EquicontinuousWithinAt.continuousWithinAt_of_mem theorem

 {H : Set <| X → α} {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) {f : X → α} (hf : f ∈ H) :
  ContinuousWithinAt f S x₀

Full source

protected theorem Set.EquicontinuousWithinAt.continuousWithinAt_of_mem {H : Set <| X → α}
    {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) {f : X → α} (hf : f ∈ H) :
    ContinuousWithinAt f S x₀ :=
  h.continuousWithinAt ⟨f, hf⟩

Continuity of Functions in an Equicontinuous Set at a Point Within a Subset

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a set $H$ of functions from $X$ to $\alpha$ that is equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$, then any function $f \in H$ is continuous at $x_0$ within $S$. In other words, if for every entourage $U$ in $\alpha$ there exists a neighborhood $V$ of $x_0$ in $S$ such that for all $x \in V$ and all $f \in H$, $(f(x_0), f(x)) \in U$, then each individual function $f \in H$ is continuous at $x_0$ within $S$.

Equicontinuous.continuous theorem

{F : ι → X → α} (h : Equicontinuous F) (i : ι) : Continuous (F i)

Full source

/-- Each function of an equicontinuous family is continuous. -/
theorem Equicontinuous.continuous {F : ι → X → α} (h : Equicontinuous F) (i : ι) :
    Continuous (F i) :=
  continuous_iff_continuousAt.mpr fun x => (h x).continuousAt i

Equicontinuity implies continuity for each function in the family

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. If a family of functions $F : \iota \to X \to \alpha$ is equicontinuous, then for every index $i \in \iota$, the function $F_i$ is continuous.

EquicontinuousOn.continuousOn theorem

{F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S) (i : ι) : ContinuousOn (F i) S

Full source

/-- Each function of a family equicontinuous on `S` is continuous on `S`. -/
theorem EquicontinuousOn.continuousOn {F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S)
    (i : ι) : ContinuousOn (F i) S :=
  fun x hx ↦ (h x hx).continuousWithinAt i

Equicontinuity on a subset implies continuity on that subset

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a family of functions $F : \iota \to X \to \alpha$ that is equicontinuous on a subset $S \subseteq X$, then for every index $i \in \iota$, the function $F_i$ is continuous on $S$. In other words, if for every $x_0 \in S$ and every entourage $U$ in $\alpha$, there exists a neighborhood $V$ of $x_0$ in $S$ such that for all $x \in V$ and all $i \in \iota$, $(F_i x_0, F_i x) \in U$, then each individual function $F_i$ is continuous on $S$.

Set.Equicontinuous.continuous_of_mem theorem

{H : Set <| X → α} (h : H.Equicontinuous) {f : X → α} (hf : f ∈ H) : Continuous f

Full source

protected theorem Set.Equicontinuous.continuous_of_mem {H : Set <| X → α} (h : H.Equicontinuous)
    {f : X → α} (hf : f ∈ H) : Continuous f :=
  h.continuous ⟨f, hf⟩

Continuity of functions in an equicontinuous set

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given an equicontinuous set of functions $H \subseteq (X \to \alpha)$, every function $f \in H$ is continuous. That is, if for every $x_0 \in X$ and every entourage $U$ in $\alpha$, there exists a neighborhood $V$ of $x_0$ such that for all $x \in V$ and all $f \in H$, the pair $(f(x_0), f(x))$ belongs to $U$, then each $f \in H$ is continuous.

Set.EquicontinuousOn.continuousOn_of_mem theorem

{H : Set <| X → α} {S : Set X} (h : H.EquicontinuousOn S) {f : X → α} (hf : f ∈ H) : ContinuousOn f S

Full source

protected theorem Set.EquicontinuousOn.continuousOn_of_mem {H : Set <| X → α} {S : Set X}
    (h : H.EquicontinuousOn S) {f : X → α} (hf : f ∈ H) : ContinuousOn f S :=
  h.continuousOn ⟨f, hf⟩

Continuity of functions in an equicontinuous set on a subset

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a set of functions $H \subseteq (X \to \alpha)$ that is equicontinuous on a subset $S \subseteq X$, then for any function $f \in H$, the function $f$ is continuous on $S$. In other words, if for every $x_0 \in S$ and every entourage $U$ in $\alpha$, there exists a neighborhood $V$ of $x_0$ in $S$ such that for all $x \in V$ and all $f \in H$, $(f(x_0), f(x)) \in U$, then each individual function $f \in H$ is continuous on $S$.

UniformEquicontinuous.uniformContinuous theorem

{F : ι → β → α} (h : UniformEquicontinuous F) (i : ι) : UniformContinuous (F i)

Full source

/-- Each function of a uniformly equicontinuous family is uniformly continuous. -/
theorem UniformEquicontinuous.uniformContinuous {F : ι → β → α} (h : UniformEquicontinuous F)
    (i : ι) : UniformContinuous (F i) := fun U hU =>
  mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i)

Uniform continuity of functions in a uniformly equicontinuous family

Informal description

For any uniformly equicontinuous family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces, each individual function $F_i$ in the family is uniformly continuous.

UniformEquicontinuousOn.uniformContinuousOn theorem

{F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S) (i : ι) : UniformContinuousOn (F i) S

Full source

/-- Each function of a family uniformly equicontinuous on `S` is uniformly continuous on `S`. -/
theorem UniformEquicontinuousOn.uniformContinuousOn {F : ι → β → α} {S : Set β}
    (h : UniformEquicontinuousOn F S) (i : ι) :
    UniformContinuousOn (F i) S := fun U hU =>
  mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i)

Uniform continuity of functions in a uniformly equicontinuous family on a subset

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces, and let $S \subseteq \beta$. If $F$ is uniformly equicontinuous on $S$, then for every index $i \in \iota$, the function $F_i$ is uniformly continuous on $S$.

Set.UniformEquicontinuous.uniformContinuous_of_mem theorem

{H : Set <| β → α} (h : H.UniformEquicontinuous) {f : β → α} (hf : f ∈ H) : UniformContinuous f

Full source

protected theorem Set.UniformEquicontinuous.uniformContinuous_of_mem {H : Set <| β → α}
    (h : H.UniformEquicontinuous) {f : β → α} (hf : f ∈ H) : UniformContinuous f :=
  h.uniformContinuous ⟨f, hf⟩

Uniform continuity of functions in a uniformly equicontinuous set

Informal description

Let $H$ be a set of functions from a uniform space $\beta$ to a uniform space $\alpha$. If $H$ is uniformly equicontinuous, then every function $f \in H$ is uniformly continuous.

Set.UniformEquicontinuousOn.uniformContinuousOn_of_mem theorem

 {H : Set <| β → α} {S : Set β} (h : H.UniformEquicontinuousOn S) {f : β → α} (hf : f ∈ H) : UniformContinuousOn f S

Full source

protected theorem Set.UniformEquicontinuousOn.uniformContinuousOn_of_mem {H : Set <| β → α}
    {S : Set β} (h : H.UniformEquicontinuousOn S) {f : β → α} (hf : f ∈ H) :
    UniformContinuousOn f S :=
  h.uniformContinuousOn ⟨f, hf⟩

Uniform continuity of functions in a uniformly equicontinuous set on a subset

Informal description

Let $H$ be a set of functions from a uniform space $\beta$ to a uniform space $\alpha$, and let $S \subseteq \beta$. If $H$ is uniformly equicontinuous on $S$, then for every function $f \in H$, $f$ is uniformly continuous on $S$.

EquicontinuousAt.comp theorem

{F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (u : κ → ι) : EquicontinuousAt (F ∘ u) x₀

Full source

/-- Taking sub-families preserves equicontinuity at a point. -/
theorem EquicontinuousAt.comp {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (u : κ → ι) :
    EquicontinuousAt (F ∘ u) x₀ := fun U hU => (h U hU).mono fun _ H k => H (u k)

Composition Preserves Equicontinuity at a Point

Informal description

Let $ X $ be a topological space and $ \alpha $ a uniform space. Given a family of functions $ F : \iota \to X \to \alpha $ that is equicontinuous at a point $ x_0 \in X $, and a function $ u : \kappa \to \iota $, the composed family $ F \circ u : \kappa \to X \to \alpha $ is also equicontinuous at $ x_0 $.

EquicontinuousWithinAt.comp theorem

 {F : ι → X → α} {S : Set X} {x₀ : X} (h : EquicontinuousWithinAt F S x₀) (u : κ → ι) :
  EquicontinuousWithinAt (F ∘ u) S x₀

Full source

/-- Taking sub-families preserves equicontinuity at a point within a subset. -/
theorem EquicontinuousWithinAt.comp {F : ι → X → α} {S : Set X} {x₀ : X}
    (h : EquicontinuousWithinAt F S x₀) (u : κ → ι) :
    EquicontinuousWithinAt (F ∘ u) S x₀ :=
  fun U hU ↦ (h U hU).mono fun _ H k => H (u k)

Preservation of Equicontinuity Within a Subset under Index Transformation

Informal description

Let $F : \iota \to X \to \alpha$ be a family of functions from a topological space $X$ to a uniform space $\alpha$, and let $S \subseteq X$ be a subset. If $F$ is equicontinuous at a point $x_0 \in X$ within $S$, then for any index transformation $u : \kappa \to \iota$, the composed family $F \circ u : \kappa \to X \to \alpha$ is also equicontinuous at $x_0$ within $S$.

Set.EquicontinuousAt.mono theorem

{H H' : Set <| X → α} {x₀ : X} (h : H.EquicontinuousAt x₀) (hH : H' ⊆ H) : H'.EquicontinuousAt x₀

Full source

protected theorem Set.EquicontinuousAt.mono {H H' : Set <| X → α} {x₀ : X}
    (h : H.EquicontinuousAt x₀) (hH : H' ⊆ H) : H'.EquicontinuousAt x₀ :=
  h.comp (inclusion hH)

Monotonicity of Equicontinuity at a Point for Sets of Functions

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given two sets of functions $H, H' \subseteq (X \to \alpha)$ with $H' \subseteq H$, if $H$ is equicontinuous at a point $x_0 \in X$, then $H'$ is also equicontinuous at $x_0$.

Set.EquicontinuousWithinAt.mono theorem

 {H H' : Set <| X → α} {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) (hH : H' ⊆ H) :
  H'.EquicontinuousWithinAt S x₀

Full source

protected theorem Set.EquicontinuousWithinAt.mono {H H' : Set <| X → α} {S : Set X} {x₀ : X}
    (h : H.EquicontinuousWithinAt S x₀) (hH : H' ⊆ H) : H'.EquicontinuousWithinAt S x₀ :=
  h.comp (inclusion hH)

Monotonicity of Equicontinuity Within a Subset

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $S \subseteq X$ a subset, and $x_0 \in X$ a point. Given two sets of functions $H, H' \subseteq (X \to \alpha)$ with $H' \subseteq H$, if $H$ is equicontinuous at $x_0$ within $S$, then $H'$ is also equicontinuous at $x_0$ within $S$.

Equicontinuous.comp theorem

{F : ι → X → α} (h : Equicontinuous F) (u : κ → ι) : Equicontinuous (F ∘ u)

Full source

/-- Taking sub-families preserves equicontinuity. -/
theorem Equicontinuous.comp {F : ι → X → α} (h : Equicontinuous F) (u : κ → ι) :
    Equicontinuous (F ∘ u) := fun x => (h x).comp u

Composition Preserves Equicontinuity

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. If a family of functions $F : \iota \to X \to \alpha$ is equicontinuous, then for any function $u : \kappa \to \iota$, the composed family $F \circ u : \kappa \to X \to \alpha$ is also equicontinuous.

EquicontinuousOn.comp theorem

{F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S) (u : κ → ι) : EquicontinuousOn (F ∘ u) S

Full source

/-- Taking sub-families preserves equicontinuity on a subset. -/
theorem EquicontinuousOn.comp {F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S) (u : κ → ι) :
    EquicontinuousOn (F ∘ u) S := fun x hx ↦ (h x hx).comp u

Equicontinuity on a Subset is Preserved under Index Transformation

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, and $S \subseteq X$ a subset. If a family of functions $F : \iota \to X \to \alpha$ is equicontinuous on $S$, then for any index transformation $u : \kappa \to \iota$, the composed family $F \circ u : \kappa \to X \to \alpha$ is also equicontinuous on $S$.

Set.Equicontinuous.mono theorem

{H H' : Set <| X → α} (h : H.Equicontinuous) (hH : H' ⊆ H) : H'.Equicontinuous

Full source

protected theorem Set.Equicontinuous.mono {H H' : Set <| X → α} (h : H.Equicontinuous)
    (hH : H' ⊆ H) : H'.Equicontinuous :=
  h.comp (inclusion hH)

Subset of Equicontinuous Functions is Equicontinuous

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. If a set of functions $H \subseteq (X \to \alpha)$ is equicontinuous, then any subset $H' \subseteq H$ is also equicontinuous.

Set.EquicontinuousOn.mono theorem

{H H' : Set <| X → α} {S : Set X} (h : H.EquicontinuousOn S) (hH : H' ⊆ H) : H'.EquicontinuousOn S

Full source

protected theorem Set.EquicontinuousOn.mono {H H' : Set <| X → α} {S : Set X}
    (h : H.EquicontinuousOn S) (hH : H' ⊆ H) : H'.EquicontinuousOn S :=
  h.comp (inclusion hH)

Subset of Equicontinuous Functions on a Set is Equicontinuous

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, and $S \subseteq X$ a subset. If a set of functions $H \subseteq (X \to \alpha)$ is equicontinuous on $S$, then any subset $H' \subseteq H$ is also equicontinuous on $S$.

UniformEquicontinuous.comp theorem

{F : ι → β → α} (h : UniformEquicontinuous F) (u : κ → ι) : UniformEquicontinuous (F ∘ u)

Full source

/-- Taking sub-families preserves uniform equicontinuity. -/
theorem UniformEquicontinuous.comp {F : ι → β → α} (h : UniformEquicontinuous F) (u : κ → ι) :
    UniformEquicontinuous (F ∘ u) := fun U hU => (h U hU).mono fun _ H k => H (u k)

Uniform Equicontinuity is Preserved Under Composition with Index Mapping

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces. If $F$ is uniformly equicontinuous, then for any function $u : \kappa \to \iota$, the composed family $F \circ u : \kappa \to \beta \to \alpha$ is also uniformly equicontinuous.

UniformEquicontinuousOn.comp theorem

 {F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S) (u : κ → ι) : UniformEquicontinuousOn (F ∘ u) S

Full source

/-- Taking sub-families preserves uniform equicontinuity on a subset. -/
theorem UniformEquicontinuousOn.comp {F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S)
    (u : κ → ι) : UniformEquicontinuousOn (F ∘ u) S :=
  fun U hU ↦ (h U hU).mono fun _ H k => H (u k)

Uniform Equicontinuity on a Subset is Preserved Under Composition with Index Mapping

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces, and let $S \subseteq \beta$ be a subset. If $F$ is uniformly equicontinuous on $S$, then for any function $u : \kappa \to \iota$, the composed family $F \circ u : \kappa \to \beta \to \alpha$ is also uniformly equicontinuous on $S$.

Set.UniformEquicontinuous.mono theorem

{H H' : Set <| β → α} (h : H.UniformEquicontinuous) (hH : H' ⊆ H) : H'.UniformEquicontinuous

Full source

protected theorem Set.UniformEquicontinuous.mono {H H' : Set <| β → α} (h : H.UniformEquicontinuous)
    (hH : H' ⊆ H) : H'.UniformEquicontinuous :=
  h.comp (inclusion hH)

Uniform Equicontinuity is Preserved Under Subset Inclusion

Informal description

Let $H$ and $H'$ be sets of functions from a uniform space $\beta$ to a uniform space $\alpha$. If $H$ is uniformly equicontinuous and $H' \subseteq H$, then $H'$ is also uniformly equicontinuous.

Set.UniformEquicontinuousOn.mono theorem

{H H' : Set <| β → α} {S : Set β} (h : H.UniformEquicontinuousOn S) (hH : H' ⊆ H) : H'.UniformEquicontinuousOn S

Full source

protected theorem Set.UniformEquicontinuousOn.mono {H H' : Set <| β → α} {S : Set β}
    (h : H.UniformEquicontinuousOn S) (hH : H' ⊆ H) : H'.UniformEquicontinuousOn S :=
  h.comp (inclusion hH)

Uniform Equicontinuity on Subset is Preserved Under Subset Inclusion

Informal description

Let $H$ and $H'$ be sets of functions from a uniform space $\beta$ to a uniform space $\alpha$, and let $S \subseteq \beta$. If $H$ is uniformly equicontinuous on $S$ and $H' \subseteq H$, then $H'$ is also uniformly equicontinuous on $S$.

equicontinuousAt_iff_range theorem

{F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ EquicontinuousAt ((↑) : range F → X → α) x₀

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` iff `range 𝓕` is equicontinuous at `x₀`,
i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀`. -/
theorem equicontinuousAt_iff_range {F : ι → X → α} {x₀ : X} :
    EquicontinuousAtEquicontinuousAt F x₀ ↔ EquicontinuousAt ((↑) : range F → X → α) x₀ := by
  simp only [EquicontinuousAt, forall_subtype_range_iff]

Equicontinuity at a Point is Equivalent to Equicontinuity of the Range Family

Informal description

A family of functions $F : \iota \to X \to \alpha$ is equicontinuous at a point $x_0 \in X$ if and only if the family obtained by restricting to the range of $F$, i.e., the family $(f : \text{range } F) \mapsto f : X \to \alpha$, is equicontinuous at $x_0$.

equicontinuousWithinAt_iff_range theorem

 {F : ι → X → α} {S : Set X} {x₀ : X} :
  EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((↑) : range F → X → α) S x₀

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff `range 𝓕` is equicontinuous
at `x₀` within `S`, i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀` within `S`. -/
theorem equicontinuousWithinAt_iff_range {F : ι → X → α} {S : Set X} {x₀ : X} :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((↑) : range F → X → α) S x₀ := by
  simp only [EquicontinuousWithinAt, forall_subtype_range_iff]

Equicontinuity Within Subset at Point is Equivalent to Range Equicontinuity

Informal description

A family of functions $F : \iota \to X \to \alpha$ is equicontinuous at $x_0$ within a subset $S \subseteq X$ if and only if the family obtained by restricting to the range of $F$, $(f : \text{range } F) \mapsto f : X \to \alpha$, is equicontinuous at $x_0$ within $S$. In other words, equicontinuity within a subset at a point is preserved when considering the family of functions indexed by their range rather than the original indexing type.

equicontinuous_iff_range theorem

{F : ι → X → α} : Equicontinuous F ↔ Equicontinuous ((↑) : range F → X → α)

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous iff `range 𝓕` is equicontinuous,
i.e the family `(↑) : range F → X → α` is equicontinuous. -/
theorem equicontinuous_iff_range {F : ι → X → α} :
    EquicontinuousEquicontinuous F ↔ Equicontinuous ((↑) : range F → X → α) :=
  forall_congr' fun _ => equicontinuousAt_iff_range

Equicontinuity is Equivalent to Range Equicontinuity

Informal description

A family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is equicontinuous if and only if the family obtained by restricting to the range of $F$, i.e., the family $(f : \text{range } F) \mapsto f : X \to \alpha$, is equicontinuous.

equicontinuousOn_iff_range theorem

{F : ι → X → α} {S : Set X} : EquicontinuousOn F S ↔ EquicontinuousOn ((↑) : range F → X → α) S

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff `range 𝓕` is equicontinuous on `S`,
i.e the family `(↑) : range F → X → α` is equicontinuous on `S`. -/
theorem equicontinuousOn_iff_range {F : ι → X → α} {S : Set X} :
    EquicontinuousOnEquicontinuousOn F S ↔ EquicontinuousOn ((↑) : range F → X → α) S :=
  forall_congr' fun _ ↦ forall_congr' fun _ ↦ equicontinuousWithinAt_iff_range

Equicontinuity on Subset is Equivalent to Range Equicontinuity

Informal description

A family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is equicontinuous on a subset $S \subseteq X$ if and only if the family of functions obtained by restricting to the range of $F$, denoted by $(f : \text{range } F) \mapsto f : X \to \alpha$, is equicontinuous on $S$. In other words, equicontinuity on $S$ is preserved when considering the family indexed by the range of $F$ rather than the original indexing type $\iota$.

uniformEquicontinuous_iff_range theorem

{F : ι → β → α} : UniformEquicontinuous F ↔ UniformEquicontinuous ((↑) : range F → β → α)

Full source

/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous iff `range 𝓕` is uniformly equicontinuous,
i.e the family `(↑) : range F → β → α` is uniformly equicontinuous. -/
theorem uniformEquicontinuous_iff_range {F : ι → β → α} :
    UniformEquicontinuousUniformEquicontinuous F ↔ UniformEquicontinuous ((↑) : range F → β → α) :=
  ⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h =>
    h.comp (rangeFactorization F)⟩

Uniform Equicontinuity is Equivalent to Range Uniform Equicontinuity

Informal description

A family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces is uniformly equicontinuous if and only if the family obtained by restricting to the range of $F$, denoted by $(f : \text{range } F) \mapsto f : \beta \to \alpha$, is uniformly equicontinuous.

uniformEquicontinuousOn_iff_range theorem

 {F : ι → β → α} {S : Set β} : UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((↑) : range F → β → α) S

Full source

/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff `range 𝓕` is uniformly
equicontinuous on `S`, i.e the family `(↑) : range F → β → α` is uniformly equicontinuous on `S`. -/
theorem uniformEquicontinuousOn_iff_range {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((↑) : range F → β → α) S :=
  ⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h =>
    h.comp (rangeFactorization F)⟩

Uniform Equicontinuity on Subset is Equivalent to Range Uniform Equicontinuity

Informal description

A family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces is uniformly equicontinuous on a subset $S \subseteq \beta$ if and only if the family obtained by restricting to the range of $F$, denoted by $(f \in \text{range } F) \mapsto f : \beta \to \alpha$, is uniformly equicontinuous on $S$.

equicontinuousAt_iff_continuousAt theorem

 {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ContinuousAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) x₀

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` iff the function `swap 𝓕 : X → ι → α` is
continuous at `x₀` *when `ι → α` is equipped with the topology of uniform convergence*. This is
very useful for developing the equicontinuity API, but it should not be used directly for other
purposes. -/
theorem equicontinuousAt_iff_continuousAt {F : ι → X → α} {x₀ : X} :
    EquicontinuousAtEquicontinuousAt F x₀ ↔ ContinuousAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) x₀ := by
  rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
  rfl

Equicontinuity at a Point via Continuity of Swapped Function in Uniform Convergence Topology

Informal description

A family of functions $ F : \iota \to X \to \alpha $ from a topological space $ X $ to a uniform space $ \alpha $ is equicontinuous at a point $ x_0 \in X $ if and only if the function $ \operatorname{swap} F : X \to \iota \to \alpha $, when composed with the embedding $ \iota \to \alpha \hookrightarrow \iota \toᵤ \alpha $ into the space of functions equipped with the topology of uniform convergence, is continuous at $ x_0 $.

equicontinuousWithinAt_iff_continuousWithinAt theorem

 {F : ι → X → α} {S : Set X} {x₀ : X} :
  EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) S x₀

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff the function
`swap 𝓕 : X → ι → α` is continuous at `x₀` within `S`
*when `ι → α` is equipped with the topology of uniform convergence*. This is very useful for
developing the equicontinuity API, but it should not be used directly for other purposes. -/
theorem equicontinuousWithinAt_iff_continuousWithinAt {F : ι → X → α} {S : Set X} {x₀ : X} :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔
    ContinuousWithinAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) S x₀ := by
  rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
  rfl

Equicontinuity Within a Subset via Continuity in Uniform Convergence Topology

Informal description

A family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$ if and only if the function $\operatorname{swap} F : X \to \iota \to \alpha$, when composed with the embedding $\iota \to \alpha \hookrightarrow \iota \toᵤ \alpha$ into the space of functions equipped with the topology of uniform convergence, is continuous at $x_0$ within $S$.

equicontinuous_iff_continuous theorem

{F : ι → X → α} : Equicontinuous F ↔ Continuous (ofFun ∘ Function.swap F : X → ι →ᵤ α)

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous iff the function `swap 𝓕 : X → ι → α` is
continuous *when `ι → α` is equipped with the topology of uniform convergence*. This is
very useful for developing the equicontinuity API, but it should not be used directly for other
purposes. -/
theorem equicontinuous_iff_continuous {F : ι → X → α} :
    EquicontinuousEquicontinuous F ↔ Continuous (ofFun ∘ Function.swap F : X → ι →ᵤ α) := by
  simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]

Equicontinuity Criterion via Continuous Map to Uniform Function Space

Informal description

A family of functions $F : \iota \to X \to \alpha$ from a topological space $X$ to a uniform space $\alpha$ is equicontinuous if and only if the function $\operatorname{swap} F : X \to \iota \to \alpha$, when viewed as a map from $X$ to the space $\iota \toᵤ \alpha$ of functions equipped with the topology of uniform convergence, is continuous.

equicontinuousOn_iff_continuousOn theorem

 {F : ι → X → α} {S : Set X} : EquicontinuousOn F S ↔ ContinuousOn (ofFun ∘ Function.swap F : X → ι →ᵤ α) S

Full source

/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff the function `swap 𝓕 : X → ι → α` is
continuous on `S` *when `ι → α` is equipped with the topology of uniform convergence*. This is
very useful for developing the equicontinuity API, but it should not be used directly for other
purposes. -/
theorem equicontinuousOn_iff_continuousOn {F : ι → X → α} {S : Set X} :
    EquicontinuousOnEquicontinuousOn F S ↔ ContinuousOn (ofFun ∘ Function.swap F : X → ι →ᵤ α) S := by
  simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt]

Equicontinuity on a Subset via Uniform Convergence Topology

Informal description

A family of functions $F : \iota \to X \to \alpha$ is equicontinuous on a subset $S \subseteq X$ if and only if the function $\operatorname{swap} F : X \to \iota \to \alpha$, when viewed as a map into the space $\iota \toᵤ \alpha$ equipped with the topology of uniform convergence, is continuous on $S$.

uniformEquicontinuous_iff_uniformContinuous theorem

 {F : ι → β → α} : UniformEquicontinuous F ↔ UniformContinuous (ofFun ∘ Function.swap F : β → ι →ᵤ α)

Full source

/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous iff the function `swap 𝓕 : β → ι → α` is
uniformly continuous *when `ι → α` is equipped with the uniform structure of uniform convergence*.
This is very useful for developing the equicontinuity API, but it should not be used directly
for other purposes. -/
theorem uniformEquicontinuous_iff_uniformContinuous {F : ι → β → α} :
    UniformEquicontinuousUniformEquicontinuous F ↔ UniformContinuous (ofFun ∘ Function.swap F : β → ι →ᵤ α) := by
  rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
  rfl

Uniform Equicontinuity via Uniform Continuity of Swapped Function

Informal description

A family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces is uniformly equicontinuous if and only if the function $\operatorname{swap} F : \beta \to \iota \to \alpha$, when viewed as a map from $\beta$ to the function space $\iota \toᵤ \alpha$ equipped with the uniform structure of uniform convergence, is uniformly continuous.

uniformEquicontinuousOn_iff_uniformContinuousOn theorem

 {F : ι → β → α} {S : Set β} :
  UniformEquicontinuousOn F S ↔ UniformContinuousOn (ofFun ∘ Function.swap F : β → ι →ᵤ α) S

Full source

/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff the function
`swap 𝓕 : β → ι → α` is uniformly continuous on `S`
*when `ι → α` is equipped with the uniform structure of uniform convergence*. This is very useful
for developing the equicontinuity API, but it should not be used directly for other purposes. -/
theorem uniformEquicontinuousOn_iff_uniformContinuousOn {F : ι → β → α} {S : Set β} :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔ UniformContinuousOn (ofFun ∘ Function.swap F : β → ι →ᵤ α) S := by
  rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
  rfl

Uniform Equicontinuity on a Subset via Uniform Continuity of Swapped Function

Informal description

A family of functions $F : \iota \to \beta \to \alpha$ between uniform spaces is uniformly equicontinuous on a subset $S \subseteq \beta$ if and only if the function $\operatorname{swap} F : \beta \to \iota \to \alpha$, when viewed as a map into the space $\iota \toᵤ \alpha$ equipped with the uniform structure of uniform convergence, is uniformly continuous on $S$.

equicontinuousWithinAt_iInf_rng theorem

 {u : κ → UniformSpace α'} {F : ι → X → α'} {S : Set X} {x₀ : X} :
  EquicontinuousWithinAt (uα := ⨅ k, u k) F S x₀ ↔ ∀ k, EquicontinuousWithinAt (uα := u k) F S x₀

Full source

theorem equicontinuousWithinAt_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'}
    {S : Set X} {x₀ : X} : EquicontinuousWithinAtEquicontinuousWithinAt (uα :=  ⨅ k, u k) F S x₀ ↔
      ∀ k, EquicontinuousWithinAt (uα :=  u k) F S x₀ := by
  simp only [equicontinuousWithinAt_iff_continuousWithinAt (uα := _), topologicalSpace]
  unfold ContinuousWithinAt
  rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]

Equicontinuity Within a Subset Under Infimum of Uniform Structures

Informal description

Let $X$ be a topological space, $\alpha'$ a type equipped with a family of uniform space structures $(u_k)_{k \in \kappa}$, and $F : \iota \to X \to \alpha'$ a family of functions. For any subset $S \subseteq X$ and point $x_0 \in X$, the family $F$ is equicontinuous at $x_0$ within $S$ with respect to the infimum uniform structure $\bigsqcap_k u_k$ if and only if $F$ is equicontinuous at $x_0$ within $S$ with respect to each individual uniform structure $u_k$.

equicontinuousAt_iInf_rng theorem

 {u : κ → UniformSpace α'} {F : ι → X → α'} {x₀ : X} :
  EquicontinuousAt (uα := ⨅ k, u k) F x₀ ↔ ∀ k, EquicontinuousAt (uα := u k) F x₀

Full source

theorem equicontinuousAt_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'}
    {x₀ : X} :
    EquicontinuousAtEquicontinuousAt (uα := ⨅ k, u k) F x₀ ↔ ∀ k, EquicontinuousAt (uα := u k) F x₀ := by
  simp only [← equicontinuousWithinAt_univ (uα := _), equicontinuousWithinAt_iInf_rng]

Equicontinuity at a Point is Preserved Under Infimum of Uniform Structures

Informal description

Let $X$ be a topological space, $\alpha'$ a type equipped with a family of uniform space structures $(u_k)_{k \in \kappa}$, and $F : \iota \to X \to \alpha'$ a family of functions. For any point $x_0 \in X$, the family $F$ is equicontinuous at $x_0$ with respect to the infimum uniform structure $\bigsqcap_k u_k$ if and only if $F$ is equicontinuous at $x_0$ with respect to each individual uniform structure $u_k$.

equicontinuous_iInf_rng theorem

 {u : κ → UniformSpace α'} {F : ι → X → α'} : Equicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, Equicontinuous (uα := u k) F

Full source

theorem equicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'} :
    EquicontinuousEquicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, Equicontinuous (uα := u k) F := by
  simp_rw [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace]
  rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]

Equicontinuity Criterion via Infimum of Uniform Structures

Informal description

Let $X$ be a topological space, $\alpha'$ a type equipped with a family of uniform space structures $(u_k)_{k \in \kappa}$, and $F : \iota \to X \to \alpha'$ a family of functions. The family $F$ is equicontinuous with respect to the infimum uniform structure $\bigsqcap_k u_k$ if and only if $F$ is equicontinuous with respect to each individual uniform structure $u_k$.

equicontinuousOn_iInf_rng theorem

 {u : κ → UniformSpace α'} {F : ι → X → α'} {S : Set X} :
  EquicontinuousOn (uα := ⨅ k, u k) F S ↔ ∀ k, EquicontinuousOn (uα := u k) F S

Full source

theorem equicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'}
    {S : Set X} :
    EquicontinuousOnEquicontinuousOn (uα := ⨅ k, u k) F S ↔ ∀ k, EquicontinuousOn (uα := u k) F S := by
  simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_swap _ κ]

Equicontinuity on a Subset is Preserved Under Infimum of Uniform Structures

Informal description

Let $X$ be a topological space, $\alpha'$ a type equipped with a family of uniform space structures $(u_k)_{k \in \kappa}$, and $F : \iota \to X \to \alpha'$ a family of functions. For any subset $S \subseteq X$, the family $F$ is equicontinuous on $S$ with respect to the infimum uniform structure $\bigsqcap_k u_k$ if and only if $F$ is equicontinuous on $S$ with respect to each individual uniform structure $u_k$.

uniformEquicontinuous_iInf_rng theorem

 {u : κ → UniformSpace α'} {F : ι → β → α'} :
  UniformEquicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, UniformEquicontinuous (uα := u k) F

Full source

theorem uniformEquicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'} :
    UniformEquicontinuousUniformEquicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, UniformEquicontinuous (uα := u k) F := by
  simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)]
  rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng]

Uniform Equicontinuity is Preserved Under Infimum of Uniform Structures

Informal description

Let $\{u_k\}_{k \in \kappa}$ be a family of uniform structures on a type $\alpha'$, and let $F : \iota \to \beta \to \alpha'$ be a family of functions between uniform spaces. The family $F$ is uniformly equicontinuous with respect to the infimum uniform structure $\bigsqcap_k u_k$ if and only if $F$ is uniformly equicontinuous with respect to each individual uniform structure $u_k$.

uniformEquicontinuousOn_iInf_rng theorem

 {u : κ → UniformSpace α'} {F : ι → β → α'} {S : Set β} :
  UniformEquicontinuousOn (uα := ⨅ k, u k) F S ↔ ∀ k, UniformEquicontinuousOn (uα := u k) F S

Full source

theorem uniformEquicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'}
    {S : Set β} : UniformEquicontinuousOnUniformEquicontinuousOn (uα := ⨅ k, u k) F S ↔
      ∀ k, UniformEquicontinuousOn (uα := u k) F S := by
  simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)]
  unfold UniformContinuousOn
  rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]

Uniform Equicontinuity on a Subset is Preserved Under Infimum of Uniform Structures

Informal description

Let $\{u_k\}_{k \in \kappa}$ be a family of uniform structures on a type $\alpha'$, and let $F : \iota \to \beta \to \alpha'$ be a family of functions between uniform spaces. For any subset $S \subseteq \beta$, the family $F$ is uniformly equicontinuous on $S$ with respect to the infimum uniform structure $\bigsqcap_k u_k$ if and only if $F$ is uniformly equicontinuous on $S$ with respect to each individual uniform structure $u_k$.

equicontinuousWithinAt_iInf_dom theorem

 {t : κ → TopologicalSpace X'} {F : ι → X' → α} {S : Set X'} {x₀ : X'} {k : κ}
  (hk : EquicontinuousWithinAt (tX := t k) F S x₀) : EquicontinuousWithinAt (tX := ⨅ k, t k) F S x₀

Full source

theorem equicontinuousWithinAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α}
    {S : Set X'} {x₀ : X'} {k : κ} (hk : EquicontinuousWithinAt (tX := t k) F S x₀) :
    EquicontinuousWithinAt (tX := ⨅ k, t k) F S x₀ := by
  simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢
  unfold ContinuousWithinAt nhdsWithin at hk ⊢
  rw [nhds_iInf]
  exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Equicontinuity Within a Subset is Preserved Under Infimum of Topologies

Informal description

Let $\{t_k\}_{k \in \kappa}$ be a family of topologies on a type $X'$, and let $F : \iota \to X' \to \alpha$ be a family of functions from $X'$ to a uniform space $\alpha$. For any subset $S \subseteq X'$ and point $x_0 \in X'$, if $F$ is equicontinuous at $x_0$ within $S$ with respect to the topology $t_k$ for some $k \in \kappa$, then $F$ is also equicontinuous at $x_0$ within $S$ with respect to the infimum topology $\bigsqcap_{k} t_k$.

equicontinuousAt_iInf_dom theorem

 {t : κ → TopologicalSpace X'} {F : ι → X' → α} {x₀ : X'} {k : κ} (hk : EquicontinuousAt (tX := t k) F x₀) :
  EquicontinuousAt (tX := ⨅ k, t k) F x₀

Full source

theorem equicontinuousAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α}
    {x₀ : X'} {k : κ} (hk : EquicontinuousAt (tX := t k) F x₀) :
    EquicontinuousAt (tX := ⨅ k, t k) F x₀ := by
  rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢
  exact equicontinuousWithinAt_iInf_dom hk

Equicontinuity at a Point is Preserved Under Infimum of Topologies

Informal description

Let $\{t_k\}_{k \in \kappa}$ be a family of topologies on a type $X'$, and let $F : \iota \to X' \to \alpha$ be a family of functions from $X'$ to a uniform space $\alpha$. For a point $x_0 \in X'$, if $F$ is equicontinuous at $x_0$ with respect to the topology $t_k$ for some $k \in \kappa$, then $F$ is also equicontinuous at $x_0$ with respect to the infimum topology $\bigsqcap_{k} t_k$.

equicontinuous_iInf_dom theorem

 {t : κ → TopologicalSpace X'} {F : ι → X' → α} {k : κ} (hk : Equicontinuous (tX := t k) F) :
  Equicontinuous (tX := ⨅ k, t k) F

Full source

theorem equicontinuous_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α}
    {k : κ} (hk : Equicontinuous (tX := t k) F) :
    Equicontinuous (tX := ⨅ k, t k) F :=
  fun x ↦ equicontinuousAt_iInf_dom (hk x)

Equicontinuity is Preserved Under Infimum of Topologies

Informal description

Let $\{t_k\}_{k \in \kappa}$ be a family of topologies on a type $X'$, and let $F : \iota \to X' \to \alpha$ be a family of functions from $X'$ to a uniform space $\alpha$. If $F$ is equicontinuous with respect to the topology $t_k$ for some $k \in \kappa$, then $F$ is also equicontinuous with respect to the infimum topology $\bigsqcap_{k} t_k$.

equicontinuousOn_iInf_dom theorem

 {t : κ → TopologicalSpace X'} {F : ι → X' → α} {S : Set X'} {k : κ} (hk : EquicontinuousOn (tX := t k) F S) :
  EquicontinuousOn (tX := ⨅ k, t k) F S

Full source

theorem equicontinuousOn_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α}
    {S : Set X'} {k : κ} (hk : EquicontinuousOn (tX := t k) F S) :
    EquicontinuousOn (tX := ⨅ k, t k) F S :=
  fun x hx ↦ equicontinuousWithinAt_iInf_dom (hk x hx)

Equicontinuity on a Subset is Preserved Under Infimum of Topologies

Informal description

Let $\{t_k\}_{k \in \kappa}$ be a family of topologies on a type $X'$, and let $F : \iota \to X' \to \alpha$ be a family of functions from $X'$ to a uniform space $\alpha$. For any subset $S \subseteq X'$, if $F$ is equicontinuous on $S$ with respect to the topology $t_k$ for some $k \in \kappa$, then $F$ is also equicontinuous on $S$ with respect to the infimum topology $\bigsqcap_{k} t_k$.

uniformEquicontinuous_iInf_dom theorem

 {u : κ → UniformSpace β'} {F : ι → β' → α} {k : κ} (hk : UniformEquicontinuous (uβ := u k) F) :
  UniformEquicontinuous (uβ := ⨅ k, u k) F

Full source

theorem uniformEquicontinuous_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α}
    {k : κ} (hk : UniformEquicontinuous (uβ := u k) F) :
    UniformEquicontinuous (uβ := ⨅ k, u k) F := by
  simp_rw [uniformEquicontinuous_iff_uniformContinuous (uβ := _)] at hk ⊢
  exact uniformContinuous_iInf_dom hk

Uniform Equicontinuity is Preserved Under Infimum of Uniform Structures

Informal description

Let $\{u_k\}_{k \in \kappa}$ be a family of uniform structures on a type $\beta'$, and let $F : \iota \to \beta' \to \alpha$ be a family of functions between uniform spaces. If $F$ is uniformly equicontinuous with respect to the uniform structure $u_k$ for some $k \in \kappa$, then $F$ is also uniformly equicontinuous with respect to the infimum uniform structure $\bigsqcap_{k} u_k$.

uniformEquicontinuousOn_iInf_dom theorem

 {u : κ → UniformSpace β'} {F : ι → β' → α} {S : Set β'} {k : κ} (hk : UniformEquicontinuousOn (uβ := u k) F S) :
  UniformEquicontinuousOn (uβ := ⨅ k, u k) F S

Full source

theorem uniformEquicontinuousOn_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α}
    {S : Set β'} {k : κ} (hk : UniformEquicontinuousOn (uβ := u k) F S) :
    UniformEquicontinuousOn (uβ := ⨅ k, u k) F S := by
  simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢
  unfold UniformContinuousOn
  rw [iInf_uniformity]
  exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Uniform Equicontinuity on a Subset is Preserved under Infimum of Uniform Structures

Informal description

Let $\{u_k\}_{k \in \kappa}$ be a family of uniform structures on a type $\beta'$, and let $F : \iota \to \beta' \to \alpha$ be a family of functions between uniform spaces. For a subset $S \subseteq \beta'$ and a fixed index $k \in \kappa$, if $F$ is uniformly equicontinuous on $S$ with respect to the uniform structure $u_k$, then $F$ is also uniformly equicontinuous on $S$ with respect to the infimum uniform structure $\bigsqcap_{k} u_k$.

Filter.HasBasis.equicontinuousAt_iff_left theorem

 {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p s) :
  EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U

Full source

theorem Filter.HasBasis.equicontinuousAt_iff_left {p : κ → Prop} {s : κ → Set X}
    {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p s) :
    EquicontinuousAtEquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U := by
  rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
  rfl

Equicontinuity at a Point via Neighborhood Basis Characterization

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a family of functions $F : \iota \to X \to \alpha$, a point $x_0 \in X$, and a basis $\{s_k\}_{k \in \kappa}$ for the neighborhood filter $\mathcal{N}(x_0)$ indexed by predicates $\{p_k\}_{k \in \kappa}$, the family $F$ is equicontinuous at $x_0$ if and only if for every entourage $U$ in the uniformity $\mathcal{U}(\alpha)$ of $\alpha$, there exists an index $k \in \kappa$ such that $p_k$ holds and for all $x \in s_k$ and all indices $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $U$.

Filter.HasBasis.equicontinuousWithinAt_iff_left theorem

 {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {S : Set X} {x₀ : X} (hX : (𝓝[S] x₀).HasBasis p s) :
  EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U

Full source

theorem Filter.HasBasis.equicontinuousWithinAt_iff_left {p : κ → Prop} {s : κ → Set X}
    {F : ι → X → α} {S : Set X} {x₀ : X} (hX : (𝓝[S] x₀).HasBasis p s) :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U := by
  rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
  rfl

Characterization of Equicontinuity Within a Subset via Basis of Neighborhood Filter

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $S \subseteq X$ a subset, and $x_0 \in X$ a point. Suppose the neighborhood filter $\mathcal{N}_S(x_0)$ has a basis $\{s_k\}_{k \in \kappa}$ indexed by a predicate $p : \kappa \to \text{Prop}$. Then, a family of functions $F : \iota \to X \to \alpha$ is equicontinuous at $x_0$ within $S$ if and only if for every entourage $U$ in the uniformity $\mathcal{U}(\alpha)$ of $\alpha$, there exists an index $k \in \kappa$ such that $p(k)$ holds and for all $x \in s_k$ and all indices $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $U$.

Filter.HasBasis.equicontinuousAt_iff_right theorem

 {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hα : (𝓤 α).HasBasis p s) :
  EquicontinuousAt F x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ s k

Full source

theorem Filter.HasBasis.equicontinuousAt_iff_right {p : κ → Prop} {s : κ → Set (α × α)}
    {F : ι → X → α} {x₀ : X} (hα : (𝓤 α).HasBasis p s) :
    EquicontinuousAtEquicontinuousAt F x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ s k := by
  rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
  rfl

Equicontinuity at a Point via Basis of Uniformity

Informal description

Let $ \alpha $ be a uniform space with a basis $ \{s_k\}_{k \in \kappa} $ for its uniformity $ \mathcal{U}(\alpha) $, indexed by a type $ \kappa $ with a predicate $ p : \kappa \to \text{Prop} $. A family of functions $ F : \iota \to X \to \alpha $ from a topological space $ X $ to $ \alpha $ is equicontinuous at a point $ x_0 \in X $ if and only if for every $ k \in \kappa $ such that $ p(k) $ holds, there exists a neighborhood $ V $ of $ x_0 $ such that for all $ x \in V $ and all $ i \in \iota $, the pair $ (F_i x_0, F_i x) $ belongs to $ s_k $.

Filter.HasBasis.equicontinuousWithinAt_iff_right theorem

 {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X} (hα : (𝓤 α).HasBasis p s) :
  EquicontinuousWithinAt F S x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ s k

Full source

theorem Filter.HasBasis.equicontinuousWithinAt_iff_right {p : κ → Prop}
    {s : κ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X} (hα : (𝓤 α).HasBasis p s) :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ s k := by
  rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
  rfl

Characterization of Equicontinuity Within a Subset via Uniformity Basis

Informal description

Let $\alpha$ be a uniform space with a basis $\{s(k) \mid p(k)\}$ for its uniformity $\mathcal{U}(\alpha)$. A family of functions $F : \iota \to X \to \alpha$ is equicontinuous at a point $x_0 \in X$ within a subset $S \subseteq X$ if and only if for every index $k$ such that $p(k)$ holds, there exists a neighborhood $V$ of $x_0$ within $S$ such that for all $x \in V$ and all $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $s(k)$. In other words, equicontinuity within $S$ at $x_0$ is equivalent to the condition that for every uniformity basis set $s(k)$ (with $p(k)$), the functions $F_i$ simultaneously satisfy the $s(k)$-closeness condition in a neighborhood of $x_0$ within $S$.

Filter.HasBasis.equicontinuousAt_iff theorem

 {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {x₀ : X}
  (hX : (𝓝 x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
  EquicontinuousAt F x₀ ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂

Full source

theorem Filter.HasBasis.equicontinuousAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X}
    {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p₁ s₁)
    (hα : (𝓤 α).HasBasis p₂ s₂) :
    EquicontinuousAtEquicontinuousAt F x₀ ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂ := by
  rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
  rfl

Equicontinuity at a Point via Basis Characterization

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Consider a family of functions $F : \iota \to X \to \alpha$ and a point $x_0 \in X$. Suppose $\mathcal{N}(x_0)$ has a basis $\{s_1(k_1) \mid p_1(k_1)\}$ indexed by $\kappa_1$, and the uniformity $\mathcal{U}(\alpha)$ has a basis $\{s_2(k_2) \mid p_2(k_2)\}$ indexed by $\kappa_2$. Then the family $F$ is equicontinuous at $x_0$ if and only if for every $k_2 \in \kappa_2$ with $p_2(k_2)$, there exists $k_1 \in \kappa_1$ with $p_1(k_1)$ such that for all $x \in s_1(k_1)$ and all $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $s_2(k_2)$.

Filter.HasBasis.equicontinuousWithinAt_iff theorem

 {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {S : Set X}
  {x₀ : X} (hX : (𝓝[S] x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
  EquicontinuousWithinAt F S x₀ ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂

Full source

theorem Filter.HasBasis.equicontinuousWithinAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop}
    {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X}
    (hX : (𝓝[S] x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
    EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂ := by
  rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
  rfl

Equicontinuity Within a Subset via Basis Characterization

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a family of functions $F : \iota \to X \to \alpha$, a subset $S \subseteq X$, and a point $x_0 \in X$, suppose: 1. The neighborhood filter $\mathcal{N}_S(x_0)$ has a basis $\{s_1(k_1) \mid p_1(k_1)\}$ indexed by $\kappa_1$ with predicate $p_1$. 2. The uniformity $\mathcal{U}(\alpha)$ has a basis $\{s_2(k_2) \mid p_2(k_2)\}$ indexed by $\kappa_2$ with predicate $p_2$. Then the family $F$ is equicontinuous at $x_0$ within $S$ if and only if for every $k_2 \in \kappa_2$ with $p_2(k_2)$, there exists $k_1 \in \kappa_1$ with $p_1(k_1)$ such that for all $x \in s_1(k_1)$ and all $i \in \iota$, the pair $(F_i x_0, F_i x)$ belongs to $s_2(k_2)$.

Filter.HasBasis.uniformEquicontinuous_iff_left theorem

 {p : κ → Prop} {s : κ → Set (β × β)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p s) :
  UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U

Full source

theorem Filter.HasBasis.uniformEquicontinuous_iff_left {p : κ → Prop}
    {s : κ → Set (β × β)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p s) :
    UniformEquicontinuousUniformEquicontinuous F ↔
      ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U := by
  rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
  simp only [Prod.forall]
  rfl

Uniform Equicontinuity Criterion via Basis of Uniformity

Informal description

Let $\beta$ be a uniform space with a basis $\{s(k) \mid p(k)\}$ for its uniformity $\mathcal{U}(\beta)$, where $p(k)$ is a predicate on the index type $\kappa$ and $s(k) \subseteq \beta \times \beta$ for each $k \in \kappa$. A family of functions $F : \iota \to \beta \to \alpha$ is uniformly equicontinuous if and only if for every entourage $U \in \mathcal{U}(\alpha)$, there exists an index $k \in \kappa$ such that $p(k)$ holds and for all $x, y \in \beta$ with $(x, y) \in s(k)$, and for all $i \in \iota$, the pair $(F_i x, F_i y)$ belongs to $U$.

Filter.HasBasis.uniformEquicontinuousOn_iff_left theorem

 {p : κ → Prop} {s : κ → Set (β × β)} {F : ι → β → α} {S : Set β} (hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s) :
  UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U

Full source

theorem Filter.HasBasis.uniformEquicontinuousOn_iff_left {p : κ → Prop}
    {s : κ → Set (β × β)} {F : ι → β → α} {S : Set β} (hβ : (𝓤𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s) :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔
      ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U := by
  rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
  simp only [Prod.forall]
  rfl

Uniform Equicontinuity on a Subset via Basis of Uniformity

Informal description

Let $\beta$ be a uniform space and $S \subseteq \beta$ a subset. Suppose the uniformity $\mathcal{U}(\beta)$ restricted to $S \times S$ has a basis $\{s(k) \mid p(k)\}$ indexed by $\kappa$. Then a family of functions $F : \iota \to \beta \to \alpha$ is uniformly equicontinuous on $S$ if and only if for every entourage $U$ in the uniformity $\mathcal{U}(\alpha)$, there exists an index $k$ such that $p(k)$ holds and for all $(x, y) \in s(k)$ and all $i \in \iota$, the pair $(F_i x, F_i y)$ belongs to $U$.

Filter.HasBasis.uniformEquicontinuous_iff_right theorem

 {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → β → α} (hα : (𝓤 α).HasBasis p s) :
  UniformEquicontinuous F ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ s k

Full source

theorem Filter.HasBasis.uniformEquicontinuous_iff_right {p : κ → Prop}
    {s : κ → Set (α × α)} {F : ι → β → α} (hα : (𝓤 α).HasBasis p s) :
    UniformEquicontinuousUniformEquicontinuous F ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ s k := by
  rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
  rfl

Uniform Equicontinuity Characterization via Basis of Target Uniformity

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $\mathfrak{B}$ be a basis for the uniformity $\mathcal{U}(\alpha)$ of $\alpha$, indexed by a type $\kappa$ with a predicate $p : \kappa \to \text{Prop}$ and a family of sets $s : \kappa \to \text{Set}(\alpha \times \alpha)$. A family of functions $F : \iota \to \beta \to \alpha$ is uniformly equicontinuous if and only if for every $k \in \kappa$ such that $p(k)$ holds, the set of pairs $(x, y) \in \beta \times \beta$ for which $(F_i x, F_i y) \in s(k)$ for all $i \in \iota$ is an entourage in the uniformity $\mathcal{U}(\beta)$ of $\beta$.

Filter.HasBasis.uniformEquicontinuousOn_iff_right theorem

 {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → β → α} {S : Set β} (hα : (𝓤 α).HasBasis p s) :
  UniformEquicontinuousOn F S ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ s k

Full source

theorem Filter.HasBasis.uniformEquicontinuousOn_iff_right {p : κ → Prop}
    {s : κ → Set (α × α)} {F : ι → β → α} {S : Set β} (hα : (𝓤 α).HasBasis p s) :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔
      ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ s k := by
  rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
  rfl

Uniform Equicontinuity on a Subset via Basis Entourages

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, $F : \iota \to \beta \to \alpha$ a family of functions, and $S \subseteq \beta$ a subset. Suppose the uniformity $\mathcal{U}(\alpha)$ has a basis $\{s(k) \mid k \in \kappa, p(k)\}$ where $p : \kappa \to \text{Prop}$ is a predicate. Then the family $F$ is uniformly equicontinuous on $S$ if and only if for every $k \in \kappa$ with $p(k)$, the set of pairs $(x,y) \in \beta \times \beta$ such that $(x,y) \in V$ for some entourage $V$ in the relative uniformity on $S \times S$ and $(F_i x, F_i y) \in s(k)$ for all $i \in \iota$ is eventually in the filter $\mathcal{U}(\beta) \sqcap \mathcal{P}(S \times S)$.

Filter.HasBasis.uniformEquicontinuous_iff theorem

 {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α}
  (hβ : (𝓤 β).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
  UniformEquicontinuous F ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂

Full source

theorem Filter.HasBasis.uniformEquicontinuous_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop}
    {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α}
    (hβ : (𝓤 β).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
    UniformEquicontinuousUniformEquicontinuous F ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂ := by
  rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
  simp only [Prod.forall]
  rfl

Uniform Equicontinuity Characterization via Uniformity Bases

Informal description

Let $\beta$ and $\alpha$ be uniform spaces with uniformity bases $\mathfrak{B}_\beta$ and $\mathfrak{B}_\alpha$ indexed by types $\kappa_1$ and $\kappa_2$ respectively, where $\mathfrak{B}_\beta$ consists of sets $s_1(k_1)$ for $k_1 \in \kappa_1$ satisfying $p_1(k_1)$, and $\mathfrak{B}_\alpha$ consists of sets $s_2(k_2)$ for $k_2 \in \kappa_2$ satisfying $p_2(k_2)$. A family of functions $F : \iota \to \beta \to \alpha$ is uniformly equicontinuous if and only if for every $k_2 \in \kappa_2$ with $p_2(k_2)$, there exists $k_1 \in \kappa_1$ with $p_1(k_1)$ such that for all $x, y \in \beta$, if $(x, y) \in s_1(k_1)$, then $(F_i x, F_i y) \in s_2(k_2)$ for all $i \in \iota$.

Filter.HasBasis.uniformEquicontinuousOn_iff theorem

 {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α}
  {S : Set β} (hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
  UniformEquicontinuousOn F S ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂

Full source

theorem Filter.HasBasis.uniformEquicontinuousOn_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop}
    {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α}
    {S : Set β} (hβ : (𝓤𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂ := by
  rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
  simp only [Prod.forall]
  rfl

Uniform Equicontinuity on a Subset via Basis Characterization

Informal description

Let $\beta$ and $\alpha$ be uniform spaces, with $\mathfrak{U}_\beta$ and $\mathfrak{U}_\alpha$ their respective uniformities. Suppose $\mathfrak{U}_\beta$ restricted to $S \times S$ has a basis $\{s_1(k_1) \mid p_1(k_1)\}$ indexed by $\kappa_1$, and $\mathfrak{U}_\alpha$ has a basis $\{s_2(k_2) \mid p_2(k_2)\}$ indexed by $\kappa_2$. For a family of functions $F : \iota \to \beta \to \alpha$ and a subset $S \subseteq \beta$, the following are equivalent: 1. The family $F$ is uniformly equicontinuous on $S$. 2. For every $k_2 \in \kappa_2$ with $p_2(k_2)$, there exists $k_1 \in \kappa_1$ with $p_1(k_1)$ such that for all $(x,y) \in s_1(k_1)$ and all $i \in \iota$, we have $(F_i x, F_i y) \in s_2(k_2)$.

IsUniformInducing.equicontinuousAt_iff theorem

 {F : ι → X → α} {x₀ : X} {u : α → β} (hu : IsUniformInducing u) :
  EquicontinuousAt F x₀ ↔ EquicontinuousAt ((u ∘ ·) ∘ F) x₀

Full source

/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is
equicontinuous at `x₀`. -/
theorem IsUniformInducing.equicontinuousAt_iff {F : ι → X → α} {x₀ : X} {u : α → β}
    (hu : IsUniformInducing u) : EquicontinuousAtEquicontinuousAt F x₀ ↔ EquicontinuousAt ((u ∘ ·) ∘ F) x₀ := by
  have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
  rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]
  rfl

Equicontinuity at a Point is Preserved by Uniform Inducing Maps

Informal description

Let $X$ be a topological space, $\alpha$ and $\beta$ uniform spaces, and $u : \alpha \to \beta$ a uniform inducing map. For a family of functions $F : \iota \to X \to \alpha$ and a point $x_0 \in X$, the following are equivalent: 1. The family $F$ is equicontinuous at $x_0$. 2. The family $u \circ F$ (where each $F_i$ is composed with $u$) is equicontinuous at $x_0$.

IsUniformInducing.equicontinuousWithinAt_iff theorem

 {F : ι → X → α} {S : Set X} {x₀ : X} {u : α → β} (hu : IsUniformInducing u) :
  EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((u ∘ ·) ∘ F) S x₀

Full source

/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` within a subset `S : Set X` iff the family `𝓕'`, obtained by composing each function
of `𝓕` by `u`, is equicontinuous at `x₀` within `S`. -/
lemma IsUniformInducing.equicontinuousWithinAt_iff {F : ι → X → α} {S : Set X} {x₀ : X} {u : α → β}
    (hu : IsUniformInducing u) : EquicontinuousWithinAtEquicontinuousWithinAt F S x₀ ↔
      EquicontinuousWithinAt ((u ∘ ·) ∘ F) S x₀ := by
  have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
  simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff]
  rfl

Equicontinuity Within Subset is Preserved by Uniform Inducing Maps

Informal description

Let $X$ be a topological space, $\alpha$ and $\beta$ uniform spaces, and $u : \alpha \to \beta$ a uniform inducing map. For a family of functions $F : \iota \to X \to \alpha$, a subset $S \subseteq X$, and a point $x_0 \in X$, the following are equivalent: 1. The family $F$ is equicontinuous at $x_0$ within $S$. 2. The family $u \circ F$ (where each $F_i$ is composed with $u$) is equicontinuous at $x_0$ within $S$. In other words, equicontinuity within a subset is preserved under composition with a uniform inducing map.

IsUniformInducing.equicontinuous_iff theorem

 {F : ι → X → α} {u : α → β} (hu : IsUniformInducing u) : Equicontinuous F ↔ Equicontinuous ((u ∘ ·) ∘ F)

Full source

/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous iff the
family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is equicontinuous. -/
lemma IsUniformInducing.equicontinuous_iff {F : ι → X → α} {u : α → β} (hu : IsUniformInducing u) :
    EquicontinuousEquicontinuous F ↔ Equicontinuous ((u ∘ ·) ∘ F) := by
  congrm ∀ x, ?_
  rw [hu.equicontinuousAt_iff]

Equicontinuity Criterion via Uniform Inducing Maps

Informal description

Let $X$ be a topological space, $\alpha$ and $\beta$ uniform spaces, and $u : \alpha \to \beta$ a uniform inducing map. For a family of functions $F : \iota \to X \to \alpha$, the following are equivalent: 1. The family $F$ is equicontinuous. 2. The family $u \circ F$ (where each $F_i$ is composed with $u$) is equicontinuous.

IsUniformInducing.equicontinuousOn_iff theorem

 {F : ι → X → α} {S : Set X} {u : α → β} (hu : IsUniformInducing u) :
  EquicontinuousOn F S ↔ EquicontinuousOn ((u ∘ ·) ∘ F) S

Full source

/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous on a
subset `S : Set X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is
equicontinuous on `S`. -/
theorem IsUniformInducing.equicontinuousOn_iff {F : ι → X → α} {S : Set X} {u : α → β}
    (hu : IsUniformInducing u) : EquicontinuousOnEquicontinuousOn F S ↔ EquicontinuousOn ((u ∘ ·) ∘ F) S := by
  congrm ∀ x ∈ S, ?_
  rw [hu.equicontinuousWithinAt_iff]

Equicontinuity on Subset is Preserved by Uniform Inducing Maps

Informal description

Let $X$ be a topological space, $\alpha$ and $\beta$ uniform spaces, and $u : \alpha \to \beta$ a uniform inducing map. For a family of functions $F : \iota \to X \to \alpha$ and a subset $S \subseteq X$, the following are equivalent: 1. The family $F$ is equicontinuous on $S$. 2. The family $u \circ F$ (where each $F_i$ is composed with $u$) is equicontinuous on $S$.

IsUniformInducing.uniformEquicontinuous_iff theorem

 {F : ι → β → α} {u : α → γ} (hu : IsUniformInducing u) : UniformEquicontinuous F ↔ UniformEquicontinuous ((u ∘ ·) ∘ F)

Full source

/-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous
iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is uniformly
equicontinuous. -/
theorem IsUniformInducing.uniformEquicontinuous_iff {F : ι → β → α} {u : α → γ}
    (hu : IsUniformInducing u) : UniformEquicontinuousUniformEquicontinuous F ↔ UniformEquicontinuous ((u ∘ ·) ∘ F) := by
  have := UniformFun.postcomp_isUniformInducing (α := ι) hu
  simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff]
  rfl

Uniform Equicontinuity Criterion via Uniform Inducing Maps

Informal description

Let $\alpha$ and $\gamma$ be uniform spaces, and let $u : \alpha \to \gamma$ be a uniform inducing map. Given a family of functions $\mathcal{F} : \iota \to \beta \to \alpha$, the following are equivalent: 1. The family $\mathcal{F}$ is uniformly equicontinuous. 2. The family $\mathcal{F}' = (u \circ \cdot) \circ \mathcal{F}$ (obtained by post-composing each function in $\mathcal{F}$ with $u$) is uniformly equicontinuous.

IsUniformInducing.uniformEquicontinuousOn_iff theorem

 {F : ι → β → α} {S : Set β} {u : α → γ} (hu : IsUniformInducing u) :
  UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((u ∘ ·) ∘ F) S

Full source

/-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous
on a subset `S : Set β` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`,
is uniformly equicontinuous on `S`. -/
theorem IsUniformInducing.uniformEquicontinuousOn_iff {F : ι → β → α} {S : Set β} {u : α → γ}
    (hu : IsUniformInducing u) :
    UniformEquicontinuousOnUniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((u ∘ ·) ∘ F) S := by
  have := UniformFun.postcomp_isUniformInducing (α := ι) hu
  simp only [uniformEquicontinuousOn_iff_uniformContinuousOn, this.uniformContinuousOn_iff]
  rfl

Uniform Equicontinuity on a Subset is Preserved by Uniform Inducing Maps

Informal description

Let $\alpha$ and $\gamma$ be uniform spaces, and let $u : \alpha \to \gamma$ be a uniform inducing map. Given a family of functions $F : \iota \to \beta \to \alpha$ and a subset $S \subseteq \beta$, the family $F$ is uniformly equicontinuous on $S$ if and only if the family $F' = u \circ F$ (obtained by post-composing each $F_i$ with $u$) is uniformly equicontinuous on $S$.

EquicontinuousWithinAt.closure' theorem

 {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X} (hA : EquicontinuousWithinAt (u ∘ (↑) : A → X → α) S x₀)
  (hu₁ : Continuous (S.restrict ∘ u)) (hu₂ : Continuous (eval x₀ ∘ u)) :
  EquicontinuousWithinAt (u ∘ (↑) : closure A → X → α) S x₀

Full source

/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S ∪ {x₀}` is continuous. Since
this will be applied to `DFunLike` types, we state it for any topological space with a map
to `X → α` satisfying the right continuity conditions. See also `Set.EquicontinuousWithinAt.closure`
for a more familiar (but weaker) statement.

Note: This could *technically* be called `EquicontinuousWithinAt.closure` without name clashes
with `Set.EquicontinuousWithinAt.closure`, but we don't do it because, even with a `protected`
marker, it would introduce ambiguities while working in namespace `Set` (e.g, in the proof of
any theorem called `Set.something`). -/
theorem EquicontinuousWithinAt.closure' {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X}
    (hA : EquicontinuousWithinAt (u ∘ (↑) : A → X → α) S x₀) (hu₁ : Continuous (S.restrict ∘ u))
    (hu₂ : Continuous (evaleval x₀ ∘ u)) :
    EquicontinuousWithinAt (u ∘ (↑) : closure A → X → α) S x₀ := by
  intro U hU
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS
  rw [SetCoe.forall] at *
  change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx
  refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prodMk ?_).trans (preimage_mono hVU)
  exact (continuous_apply ⟨x, hxS⟩).comp hu₁

Closure of Equicontinuous Family Within a Subset

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $Y$ a topological space with a map $u : Y \to X \to \alpha$, $S \subseteq X$ a subset, and $x_0 \in X$ a point. Suppose the family of functions $\{u(a) \mid a \in A\}$ is equicontinuous at $x_0$ within $S$ for some subset $A \subseteq Y$. If the following continuity conditions hold: 1. The map $S \times Y \to \alpha$ given by $(x, y) \mapsto u(y)(x)$ is continuous when restricted to $S$. 2. The evaluation map $Y \to \alpha$ at $x_0$ given by $y \mapsto u(y)(x_0)$ is continuous. Then the family $\{u(a) \mid a \in \overline{A}\}$ is also equicontinuous at $x_0$ within $S$, where $\overline{A}$ denotes the closure of $A$ in $Y$.

EquicontinuousAt.closure' theorem

 {A : Set Y} {u : Y → X → α} {x₀ : X} (hA : EquicontinuousAt (u ∘ (↑) : A → X → α) x₀) (hu : Continuous u) :
  EquicontinuousAt (u ∘ (↑) : closure A → X → α) x₀

Full source

/-- If a set of functions is equicontinuous at some `x₀`, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.EquicontinuousAt.closure` for a more familiar statement. -/
theorem EquicontinuousAt.closure' {A : Set Y} {u : Y → X → α} {x₀ : X}
    (hA : EquicontinuousAt (u ∘ (↑) : A → X → α) x₀) (hu : Continuous u) :
    EquicontinuousAt (u ∘ (↑) : closure A → X → α) x₀ := by
  rw [← equicontinuousWithinAt_univ] at hA ⊢
  exact hA.closure' (Pi.continuous_restrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)

Closure of Equicontinuous Family Preserves Equicontinuity at a Point

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, and $Y$ a topological space equipped with a map $u : Y \to (X \to \alpha)$. Suppose a subset $A \subseteq Y$ is such that the family of functions $\{u(a) \mid a \in A\}$ is equicontinuous at a point $x_0 \in X$. If the map $u$ is continuous (with respect to the topology of pointwise convergence on $X \to \alpha$), then the family $\{u(a) \mid a \in \overline{A}\}$ is also equicontinuous at $x_0$, where $\overline{A}$ denotes the closure of $A$ in $Y$.

Set.EquicontinuousAt.closure theorem

{A : Set (X → α)} {x₀ : X} (hA : A.EquicontinuousAt x₀) : (closure A).EquicontinuousAt x₀

Full source

/-- If a set of functions is equicontinuous at some `x₀`, its closure for the product topology is
also equicontinuous at `x₀`. -/
protected theorem Set.EquicontinuousAt.closure {A : Set (X → α)} {x₀ : X}
    (hA : A.EquicontinuousAt x₀) : (closure A).EquicontinuousAt x₀ :=
  hA.closure' (u := id) continuous_id

Closure of Equicontinuous Set Preserves Equicontinuity at a Point

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Given a set $A$ of functions from $X$ to $\alpha$ that is equicontinuous at a point $x_0 \in X$, the closure of $A$ (with respect to the topology of pointwise convergence) is also equicontinuous at $x_0$.

Set.EquicontinuousWithinAt.closure theorem

 {A : Set (X → α)} {S : Set X} {x₀ : X} (hA : A.EquicontinuousWithinAt S x₀) : (closure A).EquicontinuousWithinAt S x₀

Full source

/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, its closure for the
product topology is also equicontinuous at `x₀` within `S`. This would also be true for the coarser
topology of pointwise convergence on `S ∪ {x₀}`, see `Set.EquicontinuousWithinAt.closure'`. -/
protected theorem Set.EquicontinuousWithinAt.closure {A : Set (X → α)} {S : Set X} {x₀ : X}
    (hA : A.EquicontinuousWithinAt S x₀) :
    (closure A).EquicontinuousWithinAt S x₀ :=
  hA.closure' (u := id) (Pi.continuous_restrict _) (continuous_apply _)

Closure of Equicontinuous Family Within a Subset Preserves Equicontinuity

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $A \subseteq (X \to \alpha)$ a set of functions, $S \subseteq X$ a subset, and $x_0 \in X$ a point. If the family of functions $A$ is equicontinuous at $x_0$ within $S$, then the closure of $A$ (with respect to the product topology) is also equicontinuous at $x_0$ within $S$.

Equicontinuous.closure' theorem

 {A : Set Y} {u : Y → X → α} (hA : Equicontinuous (u ∘ (↑) : A → X → α)) (hu : Continuous u) :
  Equicontinuous (u ∘ (↑) : closure A → X → α)

Full source

/-- If a set of functions is equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.Equicontinuous.closure` for a more familiar statement. -/
theorem Equicontinuous.closure' {A : Set Y} {u : Y → X → α}
    (hA : Equicontinuous (u ∘ (↑) : A → X → α)) (hu : Continuous u) :
    Equicontinuous (u ∘ (↑) : closure A → X → α) := fun x ↦ (hA x).closure' hu

Closure of an Equicontinuous Family Preserves Equicontinuity

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, and $Y$ a topological space equipped with a continuous map $u : Y \to (X \to \alpha)$. If a subset $A \subseteq Y$ is such that the family of functions $\{u(a) \mid a \in A\}$ is equicontinuous, then the family $\{u(a) \mid a \in \overline{A}\}$ is also equicontinuous, where $\overline{A}$ denotes the closure of $A$ in $Y$.

EquicontinuousOn.closure' theorem

 {A : Set Y} {u : Y → X → α} {S : Set X} (hA : EquicontinuousOn (u ∘ (↑) : A → X → α) S)
  (hu : Continuous (S.restrict ∘ u)) : EquicontinuousOn (u ∘ (↑) : closure A → X → α) S

Full source

/-- If a set of functions is equicontinuous on a set `S`, the same is true for its closure in *any*
topology for which evaluation at any `x ∈ S` is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.EquicontinuousOn.closure` for a more familiar
(but weaker) statement. -/
theorem EquicontinuousOn.closure' {A : Set Y} {u : Y → X → α} {S : Set X}
    (hA : EquicontinuousOn (u ∘ (↑) : A → X → α) S) (hu : Continuous (S.restrict ∘ u)) :
    EquicontinuousOn (u ∘ (↑) : closure A → X → α) S :=
  fun x hx ↦ (hA x hx).closure' hu <| by exact continuous_apply ⟨x, hx⟩ |>.comp hu

Closure of Equicontinuous Family on a Subset

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $Y$ a topological space with a map $u : Y \to X \to \alpha$, and $S \subseteq X$ a subset. Suppose the family of functions $\{u(a) \mid a \in A\}$ is equicontinuous on $S$ for some subset $A \subseteq Y$. If the map $S \times Y \to \alpha$ given by $(x, y) \mapsto u(y)(x)$ is continuous when restricted to $S$, then the family $\{u(a) \mid a \in \overline{A}\}$ is also equicontinuous on $S$, where $\overline{A}$ denotes the closure of $A$ in $Y$.

Set.Equicontinuous.closure theorem

{A : Set <| X → α} (hA : A.Equicontinuous) : (closure A).Equicontinuous

Full source

/-- If a set of functions is equicontinuous, its closure for the product topology is also
equicontinuous. -/
protected theorem Set.Equicontinuous.closure {A : Set <| X → α} (hA : A.Equicontinuous) :
    (closure A).Equicontinuous := fun x ↦ Set.EquicontinuousAt.closure (hA x)

Closure of Equicontinuous Set is Equicontinuous

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. If a set of functions $A \subseteq (X \to \alpha)$ is equicontinuous, then its closure (with respect to the topology of pointwise convergence) is also equicontinuous.

Set.EquicontinuousOn.closure theorem

{A : Set <| X → α} {S : Set X} (hA : A.EquicontinuousOn S) : (closure A).EquicontinuousOn S

Full source

/-- If a set of functions is equicontinuous, its closure for the product topology is also
equicontinuous. This would also be true for the coarser topology of pointwise convergence on `S`,
see `EquicontinuousOn.closure'`. -/
protected theorem Set.EquicontinuousOn.closure {A : Set <| X → α} {S : Set X}
    (hA : A.EquicontinuousOn S) : (closure A).EquicontinuousOn S :=
  fun x hx ↦ Set.EquicontinuousWithinAt.closure (hA x hx)

Closure of Equicontinuous Family Preserves Equicontinuity on a Subset

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $A \subseteq (X \to \alpha)$ a set of functions, and $S \subseteq X$ a subset. If the family of functions $A$ is equicontinuous on $S$, then the closure of $A$ (with respect to the product topology) is also equicontinuous on $S$.

UniformEquicontinuousOn.closure' theorem

 {A : Set Y} {u : Y → β → α} {S : Set β} (hA : UniformEquicontinuousOn (u ∘ (↑) : A → β → α) S)
  (hu : Continuous (S.restrict ∘ u)) : UniformEquicontinuousOn (u ∘ (↑) : closure A → β → α) S

Full source

/-- If a set of functions is uniformly equicontinuous on a set `S`, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S` i continuous. Since this will be
applied to `DFunLike` types, we state it for any topological space with a map to `β → α` satisfying
the right continuity conditions. See also `Set.UniformEquicontinuousOn.closure` for a more familiar
(but weaker) statement. -/
theorem UniformEquicontinuousOn.closure' {A : Set Y} {u : Y → β → α} {S : Set β}
    (hA : UniformEquicontinuousOn (u ∘ (↑) : A → β → α) S) (hu : Continuous (S.restrict ∘ u)) :
    UniformEquicontinuousOn (u ∘ (↑) : closure A → β → α) S := by
  intro U hU
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)]
  rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
  rw [SetCoe.forall] at *
  change A ⊆ (fun f => (u f x, u f y)) ⁻¹' V at hxy
  refine (closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)
  · exact (continuous_apply ⟨x, hxS⟩).comp hu
  · exact (continuous_apply ⟨y, hyS⟩).comp hu

Closure of Uniformly Equicontinuous Family on a Subset

Informal description

Let $Y$ be a topological space, $\beta$ and $\alpha$ be uniform spaces, and $S \subseteq \beta$ be a subset. Given a set $A \subseteq Y$ and a map $u : Y \to \beta \to \alpha$, if the family of functions $\{u(a) \mid a \in A\}$ is uniformly equicontinuous on $S$ and the restriction map $S.\text{restrict} \circ u : Y \to S \to \alpha$ is continuous, then the family $\{u(a) \mid a \in \text{closure}(A)\}$ is also uniformly equicontinuous on $S$.

UniformEquicontinuous.closure' theorem

 {A : Set Y} {u : Y → β → α} (hA : UniformEquicontinuous (u ∘ (↑) : A → β → α)) (hu : Continuous u) :
  UniformEquicontinuous (u ∘ (↑) : closure A → β → α)

Full source

/-- If a set of functions is uniformly equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `β → α` satisfying the right
continuity conditions. See also `Set.UniformEquicontinuous.closure` for a more familiar statement.
-/
theorem UniformEquicontinuous.closure' {A : Set Y} {u : Y → β → α}
    (hA : UniformEquicontinuous (u ∘ (↑) : A → β → α)) (hu : Continuous u) :
    UniformEquicontinuous (u ∘ (↑) : closure A → β → α) := by
  rw [← uniformEquicontinuousOn_univ] at hA ⊢
  exact hA.closure' (Pi.continuous_restrict _ |>.comp hu)

Closure of Uniformly Equicontinuous Family under Continuous Extension

Informal description

Let $Y$ be a topological space, and $\beta$, $\alpha$ be uniform spaces. Given a set $A \subseteq Y$ and a map $u : Y \to \beta \to \alpha$, if the family of functions $\{u(a) \mid a \in A\}$ is uniformly equicontinuous and the map $u$ is continuous, then the family $\{u(a) \mid a \in \text{closure}(A)\}$ is also uniformly equicontinuous.

Set.UniformEquicontinuous.closure theorem

{A : Set <| β → α} (hA : A.UniformEquicontinuous) : (closure A).UniformEquicontinuous

Full source

/-- If a set of functions is uniformly equicontinuous, its closure for the product topology is also
uniformly equicontinuous. -/
protected theorem Set.UniformEquicontinuous.closure {A : Set <| β → α}
    (hA : A.UniformEquicontinuous) : (closure A).UniformEquicontinuous :=
  UniformEquicontinuous.closure' (u := id) hA continuous_id

Closure of a Uniformly Equicontinuous Set of Functions is Uniformly Equicontinuous

Informal description

Let $\beta$ and $\alpha$ be uniform spaces, and let $A$ be a set of functions from $\beta$ to $\alpha$. If $A$ is uniformly equicontinuous, then the closure of $A$ (with respect to the product topology) is also uniformly equicontinuous.

Set.UniformEquicontinuousOn.closure theorem

{A : Set <| β → α} {S : Set β} (hA : A.UniformEquicontinuousOn S) : (closure A).UniformEquicontinuousOn S

Full source

/-- If a set of functions is uniformly equicontinuous on a set `S`, its closure for the product
topology is also uniformly equicontinuous. This would also be true for the coarser topology of
pointwise convergence on `S`, see `UniformEquicontinuousOn.closure'`. -/
protected theorem Set.UniformEquicontinuousOn.closure {A : Set <| β → α} {S : Set β}
    (hA : A.UniformEquicontinuousOn S) : (closure A).UniformEquicontinuousOn S :=
  UniformEquicontinuousOn.closure' (u := id) hA (Pi.continuous_restrict _)

Closure of Uniformly Equicontinuous Set of Functions on a Subset

Informal description

Let $\beta$ and $\alpha$ be uniform spaces, $S \subseteq \beta$ a subset, and $A$ a set of functions from $\beta$ to $\alpha$. If $A$ is uniformly equicontinuous on $S$, then the closure of $A$ (with respect to the product topology) is also uniformly equicontinuous on $S$.

Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt theorem

 {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} {S : Set X} {x₀ : X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
  (h₂ : Tendsto (F · x₀) l (𝓝 (f x₀))) (h₃ : EquicontinuousWithinAt F S x₀) : ContinuousWithinAt f S x₀

Full source

/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S ∪ {x₀} : Set X`* along some nontrivial
filter, and if the family `𝓕` is equicontinuous at `x₀ : X` within `S`, then the limit is
continuous at `x₀` within `S`. -/
theorem Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt {l : Filter ι} [l.NeBot]
    {F : ι → X → α} {f : X → α} {S : Set X} {x₀ : X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
    (h₂ : Tendsto (F · x₀) l (𝓝 (f x₀))) (h₃ : EquicontinuousWithinAt F S x₀) :
    ContinuousWithinAt f S x₀ := by
  intro U hU; rw [mem_map]
  rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩
  rcases mem_uniformity_isClosed hV with ⟨W, hW, hWclosed, hWV⟩
  filter_upwards [h₃ W hW, eventually_mem_nhdsWithin] with x hx hxS using
    hVU <| ball_mono hWV (f x₀) <| hWclosed.mem_of_tendsto (h₂.prodMk_nhds (h₁ x hxS)) <|
    Eventually.of_forall hx

Continuity of Limit under Equicontinuous Convergence within a Subset

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, and $S \subseteq X$. Consider a family of functions $F_i : X \to \alpha$ indexed by $\iota$, and a function $f : X \to \alpha$. Suppose: 1. For every $x \in S$, $F_i(x)$ converges to $f(x)$ along a nontrivial filter $l$ as $i$ varies. 2. $F_i(x_0)$ converges to $f(x_0)$ along $l$ for some $x_0 \in X$. 3. The family $\{F_i\}$ is equicontinuous at $x_0$ within $S$. Then $f$ is continuous at $x_0$ within $S$.

Filter.Tendsto.continuousAt_of_equicontinuousAt theorem

 {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) :
  ContinuousAt f x₀

Full source

/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is equicontinuous at some `x₀ : X`, then the limit is continuous at `x₀`. -/
theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α}
    {f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) :
    ContinuousAt f x₀ := by
  rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at *
  exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂

Continuity of the pointwise limit of an equicontinuous family

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Consider a family of functions $F_i \colon X \to \alpha$ indexed by $\iota$, and a function $f \colon X \to \alpha$. Suppose: 1. The family $F_i$ converges pointwise to $f$ along a nontrivial filter $l$ on $\iota$. 2. The family $F_i$ is equicontinuous at a point $x_0 \in X$. Then the limit function $f$ is continuous at $x_0$.

Filter.Tendsto.continuous_of_equicontinuous theorem

 {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : Equicontinuous F) : Continuous f

Full source

/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is equicontinuous, then the limit is continuous. -/
theorem Filter.Tendsto.continuous_of_equicontinuous {l : Filter ι} [l.NeBot] {F : ι → X → α}
    {f : X → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : Equicontinuous F) : Continuous f :=
  continuous_iff_continuousAt.mpr fun x => h₁.continuousAt_of_equicontinuousAt (h₂ x)

Continuity of the pointwise limit of an equicontinuous family

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Consider a family of functions $F_i \colon X \to \alpha$ indexed by $\iota$, and a function $f \colon X \to \alpha$. Suppose: 1. The family $F_i$ converges pointwise to $f$ along a nontrivial filter $l$ on $\iota$. 2. The family $F_i$ is equicontinuous. Then the limit function $f$ is continuous.

Filter.Tendsto.continuousOn_of_equicontinuousOn theorem

 {l : Filter ι} [l.NeBot] {F : ι → X → α} {f : X → α} {S : Set X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
  (h₂ : EquicontinuousOn F S) : ContinuousOn f S

Full source

/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S : Set X`* along some nontrivial
filter, and if the family `𝓕` is equicontinuous, then the limit is continuous on `S`. -/
theorem Filter.Tendsto.continuousOn_of_equicontinuousOn {l : Filter ι} [l.NeBot] {F : ι → X → α}
    {f : X → α} {S : Set X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
    (h₂ : EquicontinuousOn F S) : ContinuousOn f S :=
  fun x hx ↦ Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt h₁ (h₁ x hx) (h₂ x hx)

Continuity of the limit of an equicontinuous family on a subset

Informal description

Let $X$ be a topological space, $\alpha$ a uniform space, $S \subseteq X$, and $F : \iota \to X \to \alpha$ a family of functions. Suppose: 1. For every $x \in S$, the net $(F_i(x))_{i \in \iota}$ converges to $f(x)$ along a nontrivial filter $l$. 2. The family $F$ is equicontinuous on $S$. Then the limit function $f$ is continuous on $S$.

Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn theorem

 {l : Filter ι} [l.NeBot] {F : ι → β → α} {f : β → α} {S : Set β} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
  (h₂ : UniformEquicontinuousOn F S) : UniformContinuousOn f S

Full source

/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise on `S : Set β`* along some nontrivial
filter, and if the family `𝓕` is uniformly equicontinuous on `S`, then the limit is uniformly
continuous on `S`. -/
theorem Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn {l : Filter ι} [l.NeBot]
    {F : ι → β → α} {f : β → α} {S : Set β} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
    (h₂ : UniformEquicontinuousOn F S) :
    UniformContinuousOn f S := by
  intro U hU; rw [mem_map]
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)]
  rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩
  exact hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prodMk_nhds (h₁ y hyS)) <|
    Eventually.of_forall hxy

Uniform continuity of the limit of a uniformly equicontinuous family on a subset

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces, and let $S \subseteq \beta$. Suppose $F$ converges pointwise to $f : \beta \to \alpha$ on $S$ along a nontrivial filter $l$ (i.e., for every $x \in S$, $\lim_{i \to l} F_i(x) = f(x)$). If $F$ is uniformly equicontinuous on $S$, then the limit function $f$ is uniformly continuous on $S$.

Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous theorem

 {l : Filter ι} [l.NeBot] {F : ι → β → α} {f : β → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) :
  UniformContinuous f

Full source

/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is uniformly equicontinuous, then the limit is uniformly continuous. -/
theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {l : Filter ι} [l.NeBot]
    {F : ι → β → α} {f : β → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) :
    UniformContinuous f := by
  rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *
  exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

Uniform continuity of the limit of a uniformly equicontinuous family

Informal description

Let $F : \iota \to \beta \to \alpha$ be a family of functions between uniform spaces, and let $f : \beta \to \alpha$ be a function. Suppose: 1. The family $F$ converges pointwise to $f$ along a nontrivial filter $l$ (i.e., $\lim_{i \to l} F_i = f$ pointwise). 2. The family $F$ is uniformly equicontinuous. Then the limit function $f$ is uniformly continuous.

EquicontinuousAt.tendsto_of_mem_closure theorem

 {l : Filter ι} {F : ι → X → α} {f : X → α} {s : Set X} {x : X} {z : α} (hF : EquicontinuousAt F x)
  (hf : Tendsto f (𝓝[s] x) (𝓝 z)) (hs : ∀ y ∈ s, Tendsto (F · y) l (𝓝 (f y))) (hx : x ∈ closure s) :
  Tendsto (F · x) l (𝓝 z)

Full source

/-- If `F : ι → X → α` is a family of functions equicontinuous at `x`,
it tends to `f y` along a filter `l` for any `y ∈ s`,
the limit function `f` tends to `z` along `𝓝[s] x`, and `x ∈ closure s`,
then `(F · x)` tends to `z` along `l`.

In some sense, this is a converse of `EquicontinuousAt.closure`. -/
theorem EquicontinuousAt.tendsto_of_mem_closure {l : Filter ι} {F : ι → X → α} {f : X → α}
    {s : Set X} {x : X} {z : α} (hF : EquicontinuousAt F x) (hf : Tendsto f (𝓝[s] x) (𝓝 z))
    (hs : ∀ y ∈ s, Tendsto (F · y) l (𝓝 (f y))) (hx : x ∈ closure s) :
    Tendsto (F · x) l (𝓝 z) := by
  rw [(nhds_basis_uniformity (𝓤 α).basis_sets).tendsto_right_iff] at hf ⊢
  intro U hU
  rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVs, hVU⟩
  rw [mem_closure_iff_nhdsWithin_neBot] at hx
  have : ∀ᶠ y in 𝓝[s] x, y ∈ s ∧ (∀ i, (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V :=
    eventually_mem_nhdsWithin.and <| ((hF V hV).filter_mono nhdsWithin_le_nhds).and (hf V hV)
  rcases this.exists with ⟨y, hys, hFy, hfy⟩
  filter_upwards [hs y hys (ball_mem_nhds _ hV)] with i hi
  exact hVU ⟨_, ⟨_, hFy i, (mem_ball_symmetry hVs).2 hi⟩, hfy⟩

Limit of Equicontinuous Family at a Point in the Closure

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Consider a family of functions $F : \iota \to X \to \alpha$ that is equicontinuous at a point $x \in X$. Suppose there exists a subset $s \subseteq X$ such that: 1. For each $y \in s$, the functions $F_i(y)$ tend to $f(y)$ along a filter $l$ as $i$ varies, 2. The limit function $f$ tends to $z$ along the neighborhood filter of $x$ relative to $s$, 3. The point $x$ belongs to the closure of $s$. Then the functions $F_i(x)$ tend to $z$ along the filter $l$ as $i$ varies.

Equicontinuous.isClosed_setOf_tendsto theorem

 {l : Filter ι} {F : ι → X → α} {f : X → α} (hF : Equicontinuous F) (hf : Continuous f) :
  IsClosed {x | Tendsto (F · x) l (𝓝 (f x))}

Full source

/-- If `F : ι → X → α` is an equicontinuous family of functions,
`f : X → α` is a continuous function, and `l` is a filter on `ι`,
then `{x | Filter.Tendsto (F · x) l (𝓝 (f x))}` is a closed set. -/
theorem Equicontinuous.isClosed_setOf_tendsto {l : Filter ι} {F : ι → X → α} {f : X → α}
    (hF : Equicontinuous F) (hf : Continuous f) :
    IsClosed {x | Tendsto (F · x) l (𝓝 (f x))} :=
  closure_subset_iff_isClosed.mp fun x hx ↦
    (hF x).tendsto_of_mem_closure (hf.continuousAt.mono_left inf_le_left) (fun _ ↦ id) hx

Closedness of the Convergence Set for an Equicontinuous Family

Informal description

Let $X$ be a topological space and $\alpha$ a uniform space. Consider an equicontinuous family of functions $F : \iota \to X \to \alpha$ and a continuous function $f : X \to \alpha$. For any filter $l$ on $\iota$, the set $\{x \in X \mid \text{the net } (F_i(x))_{i \in \iota} \text{ converges to } f(x) \text{ along } l\}$ is closed in $X$.

Mathlib.Topology.UniformSpace.Equicontinuity

Main definitions

Main statements

Notations

Implementation details

References

Tags