Mathlib.Topology.Algebra.UniformConvergence

instOneUniformFun instance

[One β] : One (α →ᵤ β)

Full source

@[to_additive] instance [One β] : One (α →ᵤ β) := Pi.instOne

Pointwise One Element on Uniform Functions

Informal description

For any type $\alpha$ and any type $\beta$ equipped with a one element $1$, the type of uniform functions $\alpha \toᵤ \beta$ is also equipped with a one element, defined pointwise as the constant function $x \mapsto 1$.

UniformFun.toFun_one theorem

[One β] : toFun (1 : α →ᵤ β) = 1

Full source

@[to_additive (attr := simp)]
lemma UniformFun.toFun_one [One β] : toFun (1 : α →ᵤ β) = 1 := rfl

Uniform Function to Function Preserves One

Informal description

For any type $\beta$ equipped with a one element $1$, the function `toFun` maps the constant uniform function $1 : \alpha \toᵤ \beta$ to the constant function $x \mapsto 1$ in $\alpha \to \beta$.

UniformFun.ofFun_one theorem

[One β] : ofFun (1 : α → β) = 1

Full source

@[to_additive (attr := simp)]
lemma UniformFun.ofFun_one [One β] : ofFun (1 : α → β) = 1 := rfl

Uniform Function Construction Preserves One Element

Informal description

For any type $\beta$ equipped with a multiplicative identity element $1$, the function `ofFun` maps the constant function $x \mapsto 1$ in $\alpha \to \beta$ to the constant uniform function $1$ in $\alpha \toᵤ \beta$.

instOneUniformOnFun instance

[One β] : One (α →ᵤ[𝔖] β)

Full source

@[to_additive] instance [One β] : One (α →ᵤ[𝔖] β) := Pi.instOne

One Element in Uniformly Convergent Function Space

Informal description

For any type $\beta$ with a one element and any family $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ with uniform convergence on $\mathfrak{S}$ has a one element given by the constant function equal to $1$.

UniformOnFun.toFun_one theorem

[One β] : toFun 𝔖 (1 : α →ᵤ[𝔖] β) = 1

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.toFun_one [One β] : toFun 𝔖 (1 : α →ᵤ[𝔖] β) = 1 := rfl

Uniformly Convergent Function Space Preserves Multiplicative Identity

Informal description

For any type $\beta$ with a multiplicative identity element $1$ and any family $\mathfrak{S}$ of subsets of $\alpha$, the function `toFun 𝔖` maps the constant function $1$ in the space $\alpha \to_{\mathfrak{S}} \beta$ of uniformly convergent functions to the multiplicative identity $1$ in $\beta$.

UniformOnFun.one_apply theorem

[One β] : ofFun 𝔖 (1 : α → β) = 1

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.one_apply [One β] : ofFun 𝔖 (1 : α → β) = 1 := rfl

Uniformly Convergent Function Space Preserves Constant One Function

Informal description

For any type $\beta$ with a multiplicative identity element $1$ and any family $\mathfrak{S}$ of subsets of $\alpha$, the function `ofFun 𝔖` maps the constant function $1 : \alpha \to \beta$ to the multiplicative identity $1$ in the space $\alpha \to_{\mathfrak{S}} \beta$ of uniformly convergent functions.

instMulUniformFun instance

[Mul β] : Mul (α →ᵤ β)

Full source

@[to_additive] instance [Mul β] : Mul (α →ᵤ β) := Pi.instMul

Pointwise Multiplication on Uniform Functions

Informal description

For any type $\alpha$ and a type $\beta$ equipped with a multiplication operation, the type $\alpha \toᵤ \beta$ of uniform functions from $\alpha$ to $\beta$ inherits a multiplication operation defined pointwise.

UniformFun.toFun_mul theorem

[Mul β] (f g : α →ᵤ β) : toFun (f * g) = toFun f * toFun g

Full source

@[to_additive (attr := simp)]
lemma UniformFun.toFun_mul [Mul β] (f g : α →ᵤ β) : toFun (f * g) = toFun f * toFun g := rfl

Preservation of Multiplication under Uniform Function Conversion

Informal description

For any type $\alpha$ and a type $\beta$ equipped with a multiplication operation, the map `toFun` from uniform functions $\alpha \toᵤ \beta$ to pointwise multiplication preserves the multiplication operation. That is, for any uniform functions $f, g : \alpha \toᵤ \beta$, we have $\text{toFun}(f * g) = \text{toFun}(f) * \text{toFun}(g)$.

UniformFun.ofFun_mul theorem

[Mul β] (f g : α → β) : ofFun (f * g) = ofFun f * ofFun g

Full source

@[to_additive (attr := simp)]
lemma UniformFun.ofFun_mul [Mul β] (f g : α → β) : ofFun (f * g) = ofFun f * ofFun g := rfl

Preservation of Pointwise Multiplication under Uniform Function Construction

Informal description

For any type $\alpha$ and a type $\beta$ equipped with a multiplication operation, the map $\text{ofFun}$ from functions $\alpha \to \beta$ to uniform functions $\alpha \toᵤ \beta$ preserves the pointwise multiplication operation. That is, for any functions $f, g : \alpha \to \beta$, we have $\text{ofFun}(f \cdot g) = \text{ofFun}(f) \cdot \text{ofFun}(g)$.

instMulUniformOnFun instance

[Mul β] : Mul (α →ᵤ[𝔖] β)

Full source

@[to_additive] instance [Mul β] : Mul (α →ᵤ[𝔖] β) := Pi.instMul

Pointwise Multiplication on Uniformly Convergent Functions

Informal description

For any type $\alpha$, a family of subsets $\mathfrak{S}$ of $\alpha$, and a type $\beta$ equipped with a multiplication operation, the space of functions $\alpha \to \beta$ with uniform convergence on $\mathfrak{S}$ inherits a multiplication operation defined pointwise.

UniformOnFun.toFun_mul theorem

[Mul β] (f g : α →ᵤ[𝔖] β) : toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.toFun_mul [Mul β] (f g : α →ᵤ[𝔖] β) :
    toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g :=
  rfl

Pointwise Multiplication Preserves Uniform $\mathfrak{S}$-Convergence

Informal description

For any type $\alpha$, a family of subsets $\mathfrak{S}$ of $\alpha$, and a type $\beta$ equipped with a multiplication operation, the pointwise product of two uniformly $\mathfrak{S}$-convergent functions $f, g : \alpha \to_{\mathfrak{S}} \beta$ equals the product of their underlying functions. That is, $\operatorname{toFun}_{\mathfrak{S}}(f \cdot g) = \operatorname{toFun}_{\mathfrak{S}}(f) \cdot \operatorname{toFun}_{\mathfrak{S}}(g)$.

UniformOnFun.ofFun_mul theorem

[Mul β] (f g : α → β) : ofFun 𝔖 (f * g) = ofFun 𝔖 f * ofFun 𝔖 g

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.ofFun_mul [Mul β] (f g : α → β) : ofFun 𝔖 (f * g) = ofFun 𝔖 f * ofFun 𝔖 g := rfl

Uniform $\mathfrak{S}$-Convergence Structure Preserves Pointwise Multiplication

Informal description

For any type $\alpha$, a family of subsets $\mathfrak{S}$ of $\alpha$, and a type $\beta$ equipped with a multiplication operation, the uniform $\mathfrak{S}$-convergence structure on the pointwise product of two functions $f, g : \alpha \to \beta$ is equal to the product of their uniform $\mathfrak{S}$-convergence structures. That is, $\operatorname{ofFun}_{\mathfrak{S}}(f \cdot g) = \operatorname{ofFun}_{\mathfrak{S}}(f) \cdot \operatorname{ofFun}_{\mathfrak{S}}(g)$.

instInvUniformFun instance

[Inv β] : Inv (α →ᵤ β)

Full source

@[to_additive] instance [Inv β] : Inv (α →ᵤ β) := Pi.instInv

Pointwise Inversion on Uniformly Convergent Functions

Informal description

For any type $α$ and any type $β$ equipped with an inversion operation, the type of uniformly convergent functions from $α$ to $β$ is also equipped with an inversion operation, defined pointwise.

UniformFun.toFun_inv theorem

[Inv β] (f : α →ᵤ β) : toFun (f⁻¹) = (toFun f)⁻¹

Full source

@[to_additive (attr := simp)]
lemma UniformFun.toFun_inv [Inv β] (f : α →ᵤ β) : toFun (f⁻¹) = (toFun f)⁻¹ := rfl

Inversion Commutes with Uniform Function Evaluation

Informal description

For any type $\beta$ equipped with an inversion operation and any uniformly convergent function $f \colon \alpha \to_{\text{u}} \beta$, the pointwise inversion of $f$ (as a function) equals the inversion of $f$ (as a uniformly convergent function). That is, $\operatorname{toFun}(f^{-1}) = (\operatorname{toFun} f)^{-1}$.

UniformFun.ofFun_inv theorem

[Inv β] (f : α → β) : ofFun (f⁻¹) = (ofFun f)⁻¹

Full source

@[to_additive (attr := simp)]
lemma UniformFun.ofFun_inv [Inv β] (f : α → β) : ofFun (f⁻¹) = (ofFun f)⁻¹ := rfl

Inversion Commutes with Uniform Function Construction

Informal description

For any type $\beta$ equipped with an inversion operation and any function $f \colon \alpha \to \beta$, the uniform function obtained by applying the inversion pointwise to $f$ is equal to the inversion of the uniform function obtained from $f$. In other words, $\text{ofFun}(f^{-1}) = (\text{ofFun}(f))^{-1}$.

instInvUniformOnFun instance

[Inv β] : Inv (α →ᵤ[𝔖] β)

Full source

@[to_additive] instance [Inv β] : Inv (α →ᵤ[𝔖] β) := Pi.instInv

Inversion Operation on Uniformly Convergent Function Spaces

Informal description

For any type $\beta$ with an inversion operation and any family $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ equipped with the uniform convergence topology inherits an inversion operation.

UniformOnFun.toFun_inv theorem

[Inv β] (f : α →ᵤ[𝔖] β) : toFun 𝔖 (f⁻¹) = (toFun 𝔖 f)⁻¹

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.toFun_inv [Inv β] (f : α →ᵤ[𝔖] β) : toFun 𝔖 (f⁻¹) = (toFun 𝔖 f)⁻¹ := rfl

Inversion Commutes with Evaluation in Uniformly Convergent Function Spaces

Informal description

For any type $\beta$ with an inversion operation and any family $\mathfrak{S}$ of subsets of $\alpha$, the inversion operation on the space of uniformly convergent functions $\alpha \to_{\mathfrak{S}} \beta$ commutes with the evaluation map, i.e., $(f^{-1})(x) = (f(x))^{-1}$ for all $x \in \alpha$.

UniformOnFun.ofFun_inv theorem

[Inv β] (f : α → β) : ofFun 𝔖 (f⁻¹) = (ofFun 𝔖 f)⁻¹

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.ofFun_inv [Inv β] (f : α → β) : ofFun 𝔖 (f⁻¹) = (ofFun 𝔖 f)⁻¹ := rfl

Inversion Commutes with Uniform Function Embedding

Informal description

For any type $\beta$ with an inversion operation and any family $\mathfrak{S}$ of subsets of $\alpha$, the inversion operation commutes with the embedding of functions into the space of uniformly convergent functions $\alpha \to_{\mathfrak{S}} \beta$. That is, for any function $f : \alpha \to \beta$, we have $\text{ofFun}_{\mathfrak{S}}(f^{-1}) = (\text{ofFun}_{\mathfrak{S}} f)^{-1}$.

instDivUniformFun instance

[Div β] : Div (α →ᵤ β)

Full source

@[to_additive] instance [Div β] : Div (α →ᵤ β) := Pi.instDiv

Pointwise Division on Uniformly Convergent Functions

Informal description

For any type $α$ and any type $β$ equipped with a division operation, the space of uniformly convergent functions $α →ᵤ β$ inherits a division operation defined pointwise.

UniformFun.toFun_div theorem

[Div β] (f g : α →ᵤ β) : toFun (f / g) = toFun f / toFun g

Full source

@[to_additive (attr := simp)]
lemma UniformFun.toFun_div [Div β] (f g : α →ᵤ β) : toFun (f / g) = toFun f / toFun g := rfl

Evaluation Preserves Pointwise Division for Uniformly Convergent Functions

Informal description

For any type $\beta$ equipped with a division operation and any uniformly convergent functions $f, g : \alpha \toᵤ \beta$, the evaluation map $\text{toFun}$ preserves division, i.e., $\text{toFun}(f / g) = \text{toFun}(f) / \text{toFun}(g)$.

UniformFun.ofFun_div theorem

[Div β] (f g : α → β) : ofFun (f / g) = ofFun f / ofFun g

Full source

@[to_additive (attr := simp)]
lemma UniformFun.ofFun_div [Div β] (f g : α → β) : ofFun (f / g) = ofFun f / ofFun g := rfl

Embedding Preserves Pointwise Division for Uniformly Convergent Functions

Informal description

For any type $\alpha$ and any type $\beta$ equipped with a division operation, the embedding `ofFun` from pointwise-divisible functions $\alpha \to \beta$ to uniformly convergent functions $\alpha \toᵤ \beta$ preserves division. That is, for any functions $f, g : \alpha \to \beta$, we have $\text{ofFun}(f/g) = \text{ofFun}(f) / \text{ofFun}(g)$.

instDivUniformOnFun instance

[Div β] : Div (α →ᵤ[𝔖] β)

Full source

@[to_additive] instance [Div β] : Div (α →ᵤ[𝔖] β) := Pi.instDiv

Pointwise Division on Uniformly Convergent Functions

Informal description

For any type $α$, collection of subsets $\mathfrak{S}$ of $α$, and type $β$ equipped with a division operation, the space of functions $α \to_{[\mathfrak{S}]} β$ with uniform convergence on $\mathfrak{S}$ inherits a division operation defined pointwise.

UniformOnFun.toFun_div theorem

[Div β] (f g : α →ᵤ[𝔖] β) : toFun 𝔖 (f / g) = toFun 𝔖 f / toFun 𝔖 g

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.toFun_div [Div β] (f g : α →ᵤ[𝔖] β) :
    toFun 𝔖 (f / g) = toFun 𝔖 f / toFun 𝔖 g :=
  rfl

Preservation of Division under Uniform Convergence Evaluation

Informal description

For any type $\alpha$, collection of subsets $\mathfrak{S}$ of $\alpha$, and type $\beta$ equipped with a division operation, the evaluation map $\text{toFun}_{\mathfrak{S}}$ from uniformly convergent functions $\alpha \to_{[\mathfrak{S}]} \beta$ to pointwise-divisible functions $\alpha \to \beta$ preserves division. That is, for any functions $f, g : \alpha \to_{[\mathfrak{S}]} \beta$, we have $\text{toFun}_{\mathfrak{S}}(f / g) = \text{toFun}_{\mathfrak{S}} f / \text{toFun}_{\mathfrak{S}} g$.

UniformOnFun.ofFun_div theorem

[Div β] (f g : α → β) : ofFun 𝔖 (f / g) = ofFun 𝔖 f / ofFun 𝔖 g

Full source

@[to_additive (attr := simp)]
lemma UniformOnFun.ofFun_div [Div β] (f g : α → β) : ofFun 𝔖 (f / g) = ofFun 𝔖 f / ofFun 𝔖 g := rfl

Preservation of Division under Uniform Convergence Embedding

Informal description

For any type $\alpha$, collection of subsets $\mathfrak{S}$ of $\alpha$, and type $\beta$ equipped with a division operation, the embedding $\text{ofFun}_{\mathfrak{S}}$ from pointwise-divisible functions $\alpha \to \beta$ to uniformly convergent functions $\alpha \to_{[\mathfrak{S}]} \beta$ preserves division. That is, for any functions $f, g : \alpha \to \beta$, we have $\text{ofFun}_{\mathfrak{S}}(f / g) = \text{ofFun}_{\mathfrak{S}} f / \text{ofFun}_{\mathfrak{S}} g$.

instMonoidUniformFun instance

[Monoid β] : Monoid (α →ᵤ β)

Full source

@[to_additive]
instance [Monoid β] : Monoid (α →ᵤ β) :=
  Pi.monoid

Monoid Structure on Uniformly Convergent Functions

Informal description

For any monoid $\beta$, the space of functions $\alpha \to \beta$ equipped with the uniform convergence topology forms a monoid under pointwise multiplication.

instMonoidUniformOnFun instance

[Monoid β] : Monoid (α →ᵤ[𝔖] β)

Full source

@[to_additive]
instance [Monoid β] : Monoid (α →ᵤ[𝔖] β) :=
  Pi.monoid

Monoid Structure on Uniformly Convergent Functions with Respect to a Collection of Subsets

Informal description

For any monoid $\beta$ and any collection $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to \beta$ equipped with the uniform convergence topology on $\mathfrak{S}$ forms a monoid under pointwise multiplication.

instCommMonoidUniformFun instance

[CommMonoid β] : CommMonoid (α →ᵤ β)

Full source

@[to_additive]
instance [CommMonoid β] : CommMonoid (α →ᵤ β) :=
  Pi.commMonoid

Commutative Monoid Structure on Uniformly Convergent Functions

Informal description

For any commutative monoid $\beta$, the space of functions $\alpha \to \beta$ equipped with the uniform convergence topology forms a commutative monoid under pointwise multiplication.

instCommMonoidUniformOnFun instance

[CommMonoid β] : CommMonoid (α →ᵤ[𝔖] β)

Full source

@[to_additive]
instance [CommMonoid β] : CommMonoid (α →ᵤ[𝔖] β) :=
  Pi.commMonoid

Commutative Monoid Structure on Uniformly Convergent Functions

Informal description

For any commutative monoid $\beta$ and any collection $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ equipped with the uniform convergence topology forms a commutative monoid.

instGroupUniformFun instance

[Group β] : Group (α →ᵤ β)

Full source

@[to_additive]
instance [Group β] : Group (α →ᵤ β) :=
  Pi.group

Group Structure on Uniformly Convergent Function Spaces

Informal description

For any group $\beta$, the space of functions $\alpha \to \beta$ equipped with the uniform convergence topology forms a group, where the group operations are defined pointwise.

instGroupUniformOnFun instance

[Group β] : Group (α →ᵤ[𝔖] β)

Full source

@[to_additive]
instance [Group β] : Group (α →ᵤ[𝔖] β) :=
  Pi.group

Group Structure on Uniformly Convergent Function Spaces

Informal description

For any group $\beta$ and any collection $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ equipped with the uniform convergence topology forms a group.

instCommGroupUniformFun instance

[CommGroup β] : CommGroup (α →ᵤ β)

Full source

@[to_additive]
instance [CommGroup β] : CommGroup (α →ᵤ β) :=
  Pi.commGroup

Commutative Group Structure on Uniformly Convergent Functions

Informal description

For any commutative group $\beta$, the space of functions $\alpha \to \beta$ with the uniform convergence topology forms a commutative group.

instCommGroupUniformOnFun instance

[CommGroup β] : CommGroup (α →ᵤ[𝔖] β)

Full source

@[to_additive]
instance [CommGroup β] : CommGroup (α →ᵤ[𝔖] β) :=
  Pi.commGroup

Commutative Group Structure on Uniformly Convergent Functions

Informal description

For any commutative group $\beta$ and any collection $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ equipped with the uniform convergence topology forms a commutative group.

instSMulUniformFun instance

{M : Type*} [SMul M β] : SMul M (α →ᵤ β)

Full source

instance {M : Type*} [SMul M β] : SMul M (α →ᵤ β) := Pi.instSMul

Scalar Multiplication on Uniformly Convergent Functions

Informal description

For any type $M$ with a scalar multiplication operation on $\beta$, the space of functions $\alpha \to \beta$ with the uniform convergence structure inherits a scalar multiplication operation from $\beta$.

UniformFun.toFun_smul theorem

{M : Type*} [SMul M β] (c : M) (f : α →ᵤ β) : toFun (c • f) = c • toFun f

Full source

@[simp]
lemma UniformFun.toFun_smul {M : Type*} [SMul M β] (c : M) (f : α →ᵤ β) :
    toFun (c • f) = c • toFun f :=
  rfl

Scalar Multiplication Commutes with Uniform Function Evaluation

Informal description

For any type $M$ with a scalar multiplication operation on $\beta$, any scalar $c \in M$, and any uniformly convergent function $f \colon \alpha \to \beta$, the evaluation of the scalar multiple $c \cdot f$ as a function equals the scalar multiple of the evaluation of $f$, i.e., $\text{toFun}(c \cdot f) = c \cdot \text{toFun}(f)$.

UniformFun.ofFun_smul theorem

{M : Type*} [SMul M β] (c : M) (f : α → β) : ofFun (c • f) = c • ofFun f

Full source

@[simp]
lemma UniformFun.ofFun_smul {M : Type*} [SMul M β] (c : M) (f : α → β) :
    ofFun (c • f) = c • ofFun f :=
  rfl

Scalar Multiplication Commutes with Uniform Function Embedding

Informal description

For any type $M$ with a scalar multiplication operation on $\beta$, and for any scalar $c \in M$ and function $f \colon \alpha \to \beta$, the uniform convergence structure's embedding `ofFun` satisfies $\text{ofFun}(c \cdot f) = c \cdot \text{ofFun}(f)$.

instSMulUniformOnFun instance

{M : Type*} [SMul M β] : SMul M (α →ᵤ[𝔖] β)

Full source

instance {M : Type*} [SMul M β] : SMul M (α →ᵤ[𝔖] β) := Pi.instSMul

Scalar Multiplication on Uniformly Convergent Functions

Informal description

For any type $M$ with a scalar multiplication operation on $\beta$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (uniformly convergent on sets in $\mathfrak{S}$) inherits a scalar multiplication structure from $\beta$.

UniformOnFun.toFun_smul theorem

{M : Type*} [SMul M β] (c : M) (f : α →ᵤ[𝔖] β) : toFun 𝔖 (c • f) = c • toFun 𝔖 f

Full source

@[simp]
lemma UniformOnFun.toFun_smul {M : Type*} [SMul M β] (c : M) (f : α →ᵤ[𝔖] β) :
    toFun 𝔖 (c • f) = c • toFun 𝔖 f :=
  rfl

Compatibility of Scalar Multiplication with Pointwise Evaluation in Uniform-on-$\mathfrak{S}$ Functions

Informal description

For any type $M$ with a scalar multiplication operation on $\beta$, any scalar $c \in M$, and any function $f \colon \alpha \to_{\mathfrak{S}} \beta$ (uniformly convergent on sets in $\mathfrak{S}$), the pointwise evaluation of the scalar multiplication $c \cdot f$ equals the scalar multiplication of $c$ with the pointwise evaluation of $f$. In symbols: $$ \text{toFun}_{\mathfrak{S}}(c \cdot f) = c \cdot \text{toFun}_{\mathfrak{S}}(f). $$

UniformOnFun.ofFun_smul theorem

{M : Type*} [SMul M β] (c : M) (f : α → β) : ofFun 𝔖 (c • f) = c • ofFun 𝔖 f

Full source

@[simp]
lemma UniformOnFun.ofFun_smul {M : Type*} [SMul M β] (c : M) (f : α → β) :
    ofFun 𝔖 (c • f) = c • ofFun 𝔖 f :=
  rfl

Compatibility of Pointwise Scalar Multiplication with Uniform-on-$\mathfrak{S}$ Construction

Informal description

For any type $M$ with a scalar multiplication operation on $\beta$, any scalar $c \in M$, and any function $f \colon \alpha \to \beta$, the uniform-on-$\mathfrak{S}$ function obtained from the pointwise scalar multiplication $c \cdot f$ is equal to the scalar multiplication of $c$ with the uniform-on-$\mathfrak{S}$ function obtained from $f$. In symbols: $$ \text{ofFun}_{\mathfrak{S}}(c \cdot f) = c \cdot \text{ofFun}_{\mathfrak{S}}(f). $$

instIsScalarTowerUniformFun instance

{M N : Type*} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] : IsScalarTower M N (α →ᵤ β)

Full source

instance {M N : Type*} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] :
    IsScalarTower M N (α →ᵤ β) :=
  Pi.isScalarTower

Scalar Tower Structure on Uniformly Convergent Functions

Informal description

For any types $M$ and $N$ with scalar multiplication operations on $\beta$ such that $M$ and $N$ form a scalar tower over $\beta$, the space of uniformly convergent functions $\alpha \to \beta$ also forms a scalar tower with $M$ and $N$.

instIsScalarTowerUniformOnFun instance

{M N : Type*} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] : IsScalarTower M N (α →ᵤ[𝔖] β)

Full source

instance {M N : Type*} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] :
    IsScalarTower M N (α →ᵤ[𝔖] β) :=
  Pi.isScalarTower

Scalar Multiplication Tower Property for Uniformly Convergent Functions

Informal description

For any types $M$ and $N$ with scalar multiplication operations on $\beta$ such that $M$ acts on $N$ and $\beta$, and the scalar multiplications satisfy the tower property $(m \cdot n) \cdot b = m \cdot (n \cdot b)$ for all $m \in M$, $n \in N$, and $b \in \beta$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (uniformly convergent on sets in $\mathfrak{S}$) inherits the tower property for scalar multiplication.

instSMulCommClassUniformFun instance

{M N : Type*} [SMul M β] [SMul N β] [SMulCommClass M N β] : SMulCommClass M N (α →ᵤ β)

Full source

instance {M N : Type*} [SMul M β] [SMul N β] [SMulCommClass M N β] :
    SMulCommClass M N (α →ᵤ β) :=
  Pi.smulCommClass

Commuting Scalar Multiplication on Uniformly Convergent Functions

Informal description

For any types $M$ and $N$ with scalar multiplication operations on $\beta$ that commute with each other, the space of functions $\alpha \to \beta$ with the uniform convergence structure inherits commuting scalar multiplication operations from $M$ and $N$.

instSMulCommClassUniformOnFun instance

{M N : Type*} [SMul M β] [SMul N β] [SMulCommClass M N β] : SMulCommClass M N (α →ᵤ[𝔖] β)

Full source

instance {M N : Type*} [SMul M β] [SMul N β] [SMulCommClass M N β] :
    SMulCommClass M N (α →ᵤ[𝔖] β) :=
  Pi.smulCommClass

Commutativity of Scalar Actions on Uniformly Convergent Functions

Informal description

For any types $M$ and $N$ with scalar multiplication operations on $\beta$ that commute with each other, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (uniformly convergent on sets in $\mathfrak{S}$) inherits a scalar multiplication structure where the actions of $M$ and $N$ commute.

instMulActionUniformFun instance

{M : Type*} [Monoid M] [MulAction M β] : MulAction M (α →ᵤ β)

Full source

instance {M : Type*} [Monoid M] [MulAction M β] : MulAction M (α →ᵤ β) := Pi.mulAction _

Multiplicative Action on Uniformly Convergent Functions

Informal description

For any monoid $M$ acting on a type $\beta$, the space of functions $\alpha \to \beta$ with the uniform convergence topology inherits a multiplicative action from $M$.

instMulActionUniformOnFun instance

{M : Type*} [Monoid M] [MulAction M β] : MulAction M (α →ᵤ[𝔖] β)

Full source

instance {M : Type*} [Monoid M] [MulAction M β] : MulAction M (α →ᵤ[𝔖] β) := Pi.mulAction _

Multiplicative Action on Uniformly Convergent Functions

Informal description

For any monoid $M$ acting on a type $\beta$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (uniformly convergent on sets in $\mathfrak{S}$) inherits a multiplicative action from $M$.

instDistribMulActionUniformFun instance

{M : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] : DistribMulAction M (α →ᵤ β)

Full source

instance {M : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] :
    DistribMulAction M (α →ᵤ β) :=
  Pi.distribMulAction _

Distributive Multiplicative Action on Uniformly Convergent Functions

Informal description

For any monoid $M$ and an additive monoid $\beta$ equipped with a distributive multiplicative action of $M$, the space of functions $\alpha \to \beta$ with the uniform convergence topology inherits a distributive multiplicative action from $M$.

instDistribMulActionUniformOnFun instance

{M : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] : DistribMulAction M (α →ᵤ[𝔖] β)

Full source

instance {M : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] :
    DistribMulAction M (α →ᵤ[𝔖] β) :=
  Pi.distribMulAction _

Distributive Multiplicative Action on Uniformly Convergent Functions

Informal description

For any monoid $M$, additive monoid $\beta$, and distributive multiplicative action of $M$ on $\beta$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (uniformly convergent on sets in $\mathfrak{S}$) inherits a distributive multiplicative action from $M$.

instModuleUniformFun instance

[Semiring R] [AddCommMonoid β] [Module R β] : Module R (α →ᵤ β)

Full source

instance [Semiring R] [AddCommMonoid β] [Module R β] : Module R (α →ᵤ β) :=
  Pi.module _ _ _

Module Structure on Uniformly Convergent Functions

Informal description

For any semiring $R$, additively commutative monoid $\beta$, and module structure of $R$ over $\beta$, the space of uniformly convergent functions $\alpha \to \beta$ inherits a canonical $R$-module structure.

instModuleUniformOnFun instance

[Semiring R] [AddCommMonoid β] [Module R β] : Module R (α →ᵤ[𝔖] β)

Full source

instance [Semiring R] [AddCommMonoid β] [Module R β] : Module R (α →ᵤ[𝔖] β) :=
  Pi.module _ _ _

Module Structure on Uniformly Convergent Functions

Informal description

For any semiring $R$, additively commutative monoid $\beta$ with an $R$-module structure, and any family $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (endowed with the uniform convergence structure on $\mathfrak{S}$) inherits an $R$-module structure.

instIsUniformGroupUniformFun instance

: IsUniformGroup (α →ᵤ G)

Full source

/-- If `G` is a uniform group, then `α →ᵤ G` is a uniform group as well. -/
@[to_additive "If `G` is a uniform additive group,
then `α →ᵤ G` is a uniform additive group as well."]
instance : IsUniformGroup (α →ᵤ G) :=
  ⟨(-- Since `(/) : G × G → G` is uniformly continuous,
    -- `UniformFun.postcomp_uniformContinuous` tells us that
    -- `((/) ∘ —) : (α →ᵤ G × G) → (α →ᵤ G)` is uniformly continuous too. By precomposing with
    -- `UniformFun.uniformEquivProdArrow`, this gives that
    -- `(/) : (α →ᵤ G) × (α →ᵤ G) → (α →ᵤ G)` is also uniformly continuous
    UniformFun.postcomp_uniformContinuous uniformContinuous_div).comp
    UniformFun.uniformEquivProdArrow.symm.uniformContinuous⟩

Uniform Group Structure on Uniformly Convergent Function Spaces

Informal description

For any uniform group $G$, the space of uniformly convergent functions $\alpha \to G$ forms a uniform group, where the group operations are defined pointwise and the uniform structure is inherited from $G$.

UniformFun.hasBasis_nhds_one_of_basis theorem

 {p : ι → Prop} {b : ι → Set G} (h : (𝓝 1 : Filter G).HasBasis p b) :
  (𝓝 1 : Filter (α →ᵤ G)).HasBasis p fun i => {f : α →ᵤ G | ∀ x, toFun f x ∈ b i}

Full source

@[to_additive]
protected theorem UniformFun.hasBasis_nhds_one_of_basis {p : ι → Prop} {b : ι → Set G}
    (h : (𝓝 1 : Filter G).HasBasis p b) :
    (𝓝 1 : Filter (α →ᵤ G)).HasBasis p fun i => { f : α →ᵤ G | ∀ x, toFun f x ∈ b i } := by
  convert UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one
  simp

Neighborhood Basis at Identity for Uniform Functions via Basis on $G$

Informal description

Let $G$ be a topological group with a neighborhood basis $\{b_i\}_{i \in \iota}$ at the identity element $1$, indexed by a predicate $p$ on $\iota$. Then the neighborhood basis at the identity in the space of uniform functions $\alpha \toᵤ G$ is given by the sets $\{f : \alpha \to G \mid \forall x, f(x) \in b_i\}$ for each $i \in \iota$ satisfying $p(i)$.

UniformFun.hasBasis_nhds_one theorem

 : (𝓝 1 : Filter (α →ᵤ G)).HasBasis (fun V : Set G => V ∈ (𝓝 1 : Filter G)) fun V => {f : α → G | ∀ x, f x ∈ V}

Full source

@[to_additive]
protected theorem UniformFun.hasBasis_nhds_one :
    (𝓝 1 : Filter (α →ᵤ G)).HasBasis (fun V : Set G => V ∈ (𝓝 1 : Filter G)) fun V =>
      { f : α → G | ∀ x, f x ∈ V } :=
  UniformFun.hasBasis_nhds_one_of_basis (basis_sets _)

Basis for Identity Neighborhood Filter in Uniform Function Space

Informal description

The neighborhood filter of the identity element in the space of uniform functions $\alpha \toᵤ G$ has a basis consisting of sets of the form $\{f : \alpha \to G \mid \forall x, f(x) \in V\}$, where $V$ ranges over all neighborhoods of the identity in $G$.

instIsUniformGroupUniformOnFun instance

: IsUniformGroup (α →ᵤ[𝔖] G)

Full source

/-- Let `𝔖 : Set (Set α)`. If `G` is a uniform group, then `α →ᵤ[𝔖] G` is a uniform group as
well. -/
@[to_additive "Let `𝔖 : Set (Set α)`. If `G` is a uniform additive group,
then `α →ᵤ[𝔖] G` is a uniform additive group as well."]
instance : IsUniformGroup (α →ᵤ[𝔖] G) :=
  ⟨(-- Since `(/) : G × G → G` is uniformly continuous,
    -- `UniformOnFun.postcomp_uniformContinuous` tells us that
    -- `((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G)` is uniformly continuous too. By precomposing with
    -- `UniformOnFun.uniformEquivProdArrow`, this gives that
    -- `(/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G)` is also uniformly continuous
    UniformOnFun.postcomp_uniformContinuous uniformContinuous_div).comp
    UniformOnFun.uniformEquivProdArrow.symm.uniformContinuous⟩

Uniform Group Structure on Uniformly Convergent Function Spaces

Informal description

For any uniform group $G$ and any collection $\mathfrak{S}$ of subsets of $\alpha$, the space of functions $\alpha \to_{\mathfrak{S}} G$ equipped with the uniform convergence topology is a uniform group.

UniformOnFun.hasBasis_nhds_one_of_basis theorem

 (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {b : ι → Set G}
  (h : (𝓝 1 : Filter G).HasBasis p b) :
  (𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
    {f : α →ᵤ[𝔖] G | ∀ x ∈ Si.1, toFun 𝔖 f x ∈ b Si.2}

Full source

@[to_additive]
protected theorem UniformOnFun.hasBasis_nhds_one_of_basis (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty)
    (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {b : ι → Set G}
    (h : (𝓝 1 : Filter G).HasBasis p b) :
    (𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis (fun Si : SetSet α × ι => Si.1 ∈ 𝔖Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
      { f : α →ᵤ[𝔖] G | ∀ x ∈ Si.1, toFun 𝔖 f x ∈ b Si.2 } := by
  convert UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <|
    h.uniformity_of_nhds_one_swapped
  simp [UniformOnFun.gen]

Basis for Identity Neighborhood Filter in Uniformly Convergent Function Space

Informal description

Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed under inclusion, and let $G$ be a topological group with a filter basis $\{b_i\}_{i \in \iota}$ for the neighborhood filter of the identity, indexed by a predicate $p$. Then the neighborhood filter of the identity in the space of functions $\alpha \to_{\mathfrak{S}} G$ (with uniform convergence on $\mathfrak{S}$) has a basis consisting of sets of the form $\{f \mid \forall x \in S, f(x) \in b_i\}$ where $S \in \mathfrak{S}$ and $p(i)$ holds.

UniformOnFun.hasBasis_nhds_one theorem

 (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
  (𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis (fun SV : Set α × Set G => SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 1 : Filter G)) fun SV =>
    {f : α →ᵤ[𝔖] G | ∀ x ∈ SV.1, f x ∈ SV.2}

Full source

@[to_additive]
protected theorem UniformOnFun.hasBasis_nhds_one (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty)
    (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
    (𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis
      (fun SV : SetSet α × Set G => SV.1 ∈ 𝔖SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 1 : Filter G)) fun SV =>
      { f : α →ᵤ[𝔖] G | ∀ x ∈ SV.1, f x ∈ SV.2 } :=
  UniformOnFun.hasBasis_nhds_one_of_basis 𝔖 h𝔖₁ h𝔖₂ (basis_sets _)

Basis for Identity Neighborhood Filter in Uniformly Convergent Function Space

Informal description

Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed under inclusion, and let $G$ be a topological group. Then the neighborhood filter of the identity in the space of functions $\alpha \to_{\mathfrak{S}} G$ (with uniform convergence on $\mathfrak{S}$) has a basis consisting of sets of the form $\{f \mid \forall x \in S, f(x) \in V\}$ where $S \in \mathfrak{S}$ and $V$ is a neighborhood of the identity in $G$.

UniformFun.uniformContinuousConstSMul instance

: UniformContinuousConstSMul M (α →ᵤ X)

Full source

instance UniformFun.uniformContinuousConstSMul :
    UniformContinuousConstSMul M (α →ᵤ X) where
  uniformContinuous_const_smul c := UniformFun.postcomp_uniformContinuous <|
    uniformContinuous_const_smul c

Uniformly Continuous Scalar Multiplication on Uniformly Convergent Functions

Informal description

For any type $M$ with a scalar multiplication operation on a uniform space $X$, the space of functions $\alpha \to X$ with the uniform convergence structure has uniformly continuous scalar multiplication. That is, for each $c \in M$, the map $f \mapsto c \cdot f$ is uniformly continuous on $\alpha \to X$.

UniformFunOn.uniformContinuousConstSMul instance

{𝔖 : Set (Set α)} : UniformContinuousConstSMul M (α →ᵤ[𝔖] X)

Full source

instance UniformFunOn.uniformContinuousConstSMul {𝔖 : Set (Set α)} :
    UniformContinuousConstSMul M (α →ᵤ[𝔖] X) where
  uniformContinuous_const_smul c := UniformOnFun.postcomp_uniformContinuous <|
    uniformContinuous_const_smul c

Uniformly Continuous Scalar Multiplication on Uniformly Convergent Functions

Informal description

For any type $M$ with a scalar multiplication operation on a uniform space $X$, the space of functions $\alpha \to_{\mathfrak{S}} X$ (uniformly convergent on sets in $\mathfrak{S}$) has uniformly continuous scalar multiplication. This means that for each $c \in M$, the map $f \mapsto c \cdot f$ is uniformly continuous on $\alpha \to_{\mathfrak{S}} X$.

Mathlib.Topology.Algebra.UniformConvergence

Main statements

Implementation notes

References

Tags