# mathlibdocumentation

topology.continuous_function.algebra

# Algebraic structures over continuous functions #

In this file we define instances of algebraic structures over the type `continuous_map α β` (denoted `C(α, β)`) of bundled continuous maps from `α` to `β`. For example, `C(α, β)` is a group when `β` is a group, a ring when `β` is a ring, etc.

For each type of algebraic structure, we also define an appropriate subobject of `α → β` with carrier `{ f : α → β | continuous f }`. For example, when `β` is a group, a subgroup `continuous_subgroup α β` of `α → β` is constructed with carrier `{ f : α → β | continuous f }`.

Note that, rather than using the derived algebraic structures on these subobjects (for example, when `β` is a group, the derived group structure on `continuous_subgroup α β`), one should use `C(α, β)` with the appropriate instance of the structure.

@[protected, instance]
def continuous_functions.set_of.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
has_coe_to_fun {f : α → β | (λ (_x : {f : α → β | continuous f}), α → β)
Equations
@[protected, instance]
def continuous_map.has_mul {α : Type u_1} {β : Type u_2} [has_mul β]  :
Equations
@[protected, instance]
def continuous_map.has_add {α : Type u_1} {β : Type u_2} [has_add β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_mul {α : Type u_1} {β : Type u_2} [has_mul β] (f g : C(α, β)) :
(f * g) = f * g
@[simp, norm_cast]
theorem continuous_map.coe_add {α : Type u_1} {β : Type u_2} [has_add β] (f g : C(α, β)) :
(f + g) = f + g
@[simp]
theorem continuous_map.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_mul γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ * f₂).comp g = f₁.comp g * f₂.comp g
@[simp]
theorem continuous_map.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_add γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
@[protected, instance]
def continuous_map.has_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
Equations
@[protected, instance]
def continuous_map.has_one {α : Type u_1} {β : Type u_2} [has_one β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_one {α : Type u_1} {β : Type u_2} [has_one β] :
1 = 1
@[simp, norm_cast]
theorem continuous_map.coe_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
0 = 0
@[simp]
theorem continuous_map.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one γ] (g : C(α, β)) :
1.comp g = 1
@[simp]
theorem continuous_map.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (g : C(α, β)) :
0.comp g = 0
@[protected, instance]
def continuous_map.has_nat_cast {α : Type u_1} {β : Type u_2} [has_nat_cast β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_nat_cast {α : Type u_1} {β : Type u_2} [has_nat_cast β] (n : ) :
@[protected, instance]
def continuous_map.has_int_cast {α : Type u_1} {β : Type u_2} [has_int_cast β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_int_cast {α : Type u_1} {β : Type u_2} [has_int_cast β] (n : ) :
@[protected, instance]
def continuous_map.has_nsmul {α : Type u_1} {β : Type u_2} [add_monoid β]  :
C(α, β)
Equations
@[protected, instance]
def continuous_map.has_pow {α : Type u_1} {β : Type u_2} [monoid β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_pow {α : Type u_1} {β : Type u_2} [monoid β] (f : C(α, β)) (n : ) :
(f ^ n) = f ^ n
@[norm_cast]
theorem continuous_map.coe_nsmul {α : Type u_1} {β : Type u_2} [add_monoid β] (f : C(α, β)) (n : ) :
(n f) = n f
@[simp]
theorem continuous_map.pow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid γ] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(f ^ n).comp g = f.comp g ^ n
theorem continuous_map.nsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_monoid γ] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(n f).comp g = n f.comp g
@[protected, instance]
def continuous_map.has_neg {α : Type u_1} {β : Type u_2} [add_group β]  :
Equations
@[protected, instance]
def continuous_map.has_inv {α : Type u_1} {β : Type u_2} [group β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_neg {α : Type u_1} {β : Type u_2} [add_group β] (f : C(α, β)) :
@[simp, norm_cast]
theorem continuous_map.coe_inv {α : Type u_1} {β : Type u_2} [group β] (f : C(α, β)) :
@[simp]
theorem continuous_map.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_group γ] (f : C(β, γ)) (g : C(α, β)) :
(-f).comp g = -f.comp g
@[simp]
theorem continuous_map.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [group γ] (f : C(β, γ)) (g : C(α, β)) :
@[protected, instance]
def continuous_map.has_div {α : Type u_1} {β : Type u_2} [has_div β]  :
Equations
@[protected, instance]
def continuous_map.has_sub {α : Type u_1} {β : Type u_2} [has_sub β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_div {α : Type u_1} {β : Type u_2} [has_div β] (f g : C(α, β)) :
(f / g) = f / g
@[simp, norm_cast]
theorem continuous_map.coe_sub {α : Type u_1} {β : Type u_2} [has_sub β] (f g : C(α, β)) :
(f - g) = f - g
@[simp]
theorem continuous_map.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_sub γ] (f g : C(β, γ)) (h : C(α, β)) :
(f - g).comp h = f.comp h - g.comp h
@[simp]
theorem continuous_map.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_div γ] (f g : C(β, γ)) (h : C(α, β)) :
(f / g).comp h = f.comp h / g.comp h
@[protected, instance]
def continuous_map.has_zsmul {α : Type u_1} {β : Type u_2} [add_group β]  :
C(α, β)
Equations
@[protected, instance]
def continuous_map.has_zpow {α : Type u_1} {β : Type u_2} [group β]  :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_zpow {α : Type u_1} {β : Type u_2} [group β] (f : C(α, β)) (z : ) :
(f ^ z) = f ^ z
@[norm_cast]
theorem continuous_map.coe_zsmul {α : Type u_1} {β : Type u_2} [add_group β] (f : C(α, β)) (z : ) :
(z f) = z f
theorem continuous_map.zsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_group γ] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(z f).comp g = z f.comp g
@[simp]
theorem continuous_map.zpow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [group γ] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(f ^ z).comp g = f.comp g ^ z

### Group stucture #

In this section we show that continuous functions valued in a topological group inherit the structure of a group.

def continuous_submonoid (α : Type u_1) (β : Type u_2) [monoid β]  :
submonoid (α → β)

The `submonoid` of continuous maps `α → β`.

Equations
def continuous_add_submonoid (α : Type u_1) (β : Type u_2) [add_monoid β]  :

The `add_submonoid` of continuous maps `α → β`.

Equations
def continuous_subgroup (α : Type u_1) (β : Type u_2) [group β]  :
subgroup (α → β)

The subgroup of continuous maps `α → β`.

Equations
def continuous_add_subgroup (α : Type u_1) (β : Type u_2) [add_group β]  :

The `add_subgroup` of continuous maps `α → β`.

Equations
@[protected, instance]
def continuous_map.add_semigroup {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.semigroup {α : Type u_1} {β : Type u_2} [semigroup β]  :
Equations
@[protected, instance]
def continuous_map.add_comm_semigroup {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.comm_semigroup {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.mul_one_class {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.add_zero_class {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.mul_zero_class {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.semigroup_with_zero {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.add_monoid {α : Type u_1} {β : Type u_2} [add_monoid β]  :
Equations
@[protected, instance]
def continuous_map.monoid {α : Type u_1} {β : Type u_2} [monoid β]  :
Equations
@[protected, instance]
def continuous_map.monoid_with_zero {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.monoid_with_zero = continuous_map.monoid_with_zero._proof_1 continuous_map.monoid_with_zero._proof_2 continuous_map.monoid_with_zero._proof_3 continuous_map.monoid_with_zero._proof_4
@[protected, instance]
def continuous_map.comm_monoid {α : Type u_1} {β : Type u_2} [comm_monoid β]  :
Equations
• continuous_map.comm_monoid = continuous_map.comm_monoid._proof_1 continuous_map.comm_monoid._proof_2 continuous_map.comm_monoid._proof_3
@[protected, instance]
def continuous_map.add_comm_monoid {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.comm_monoid_with_zero {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.comm_monoid_with_zero = continuous_map.comm_monoid_with_zero._proof_1 continuous_map.comm_monoid_with_zero._proof_2 continuous_map.comm_monoid_with_zero._proof_3 continuous_map.comm_monoid_with_zero._proof_4
@[protected, instance]
def continuous_map.has_continuous_mul {α : Type u_1} {β : Type u_2} [has_mul β]  :
@[protected, instance]
def continuous_map.has_continuous_add {α : Type u_1} {β : Type u_2} [has_add β]  :
@[simp]
theorem continuous_map.coe_fn_monoid_hom_apply {α : Type u_1} {β : Type u_2} [monoid β] (x : C(α, β)) (ᾰ : α) :
def continuous_map.coe_fn_monoid_hom {α : Type u_1} {β : Type u_2} [monoid β]  :
C(α, β) →* α → β

Coercion to a function as an `monoid_hom`. Similar to `monoid_hom.coe_fn`.

Equations
@[simp]
theorem continuous_map.coe_fn_add_monoid_hom_apply {α : Type u_1} {β : Type u_2} [add_monoid β] (x : C(α, β)) (ᾰ : α) :
def continuous_map.coe_fn_add_monoid_hom {α : Type u_1} {β : Type u_2} [add_monoid β]  :
C(α, β) →+ α → β

Coercion to a function as an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn`.

Equations
@[simp]
theorem add_monoid_hom.comp_left_continuous_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (g : β →+ γ) (hg : continuous g) (f : C(α, β)) :
@[protected]
def add_monoid_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (g : β →+ γ) (hg : continuous g) :
C(α, β) →+ C(α, γ)

Composition on the left by a (continuous) homomorphism of topological `add_monoid`s, as an `add_monoid_hom`. Similar to `add_monoid_hom.comp_left`.

Equations
@[protected]
def monoid_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (g : β →* γ) (hg : continuous g) :
C(α, β) →* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological monoids, as a `monoid_hom`. Similar to `monoid_hom.comp_left`.

Equations
@[simp]
theorem monoid_hom.comp_left_continuous_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (g : β →* γ) (hg : continuous g) (f : C(α, β)) :
hg) f = {to_fun := g, continuous_to_fun := hg}.comp f
def continuous_map.comp_monoid_hom' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(α, β)) :
C(β, γ) →* C(α, γ)

Composition on the right as a `monoid_hom`. Similar to `monoid_hom.comp_hom'`.

Equations
@[simp]
theorem continuous_map.comp_monoid_hom'_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(α, β)) (f : C(β, γ)) :
def continuous_map.comp_add_monoid_hom' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(α, β)) :
C(β, γ) →+ C(α, γ)

Composition on the right as an `add_monoid_hom`. Similar to `add_monoid_hom.comp_hom'`.

Equations
@[simp]
theorem continuous_map.comp_add_monoid_hom'_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(α, β)) (f : C(β, γ)) :
@[simp]
theorem continuous_map.coe_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp]
theorem continuous_map.coe_prod {α : Type u_1} {β : Type u_2} [comm_monoid β] {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
theorem continuous_map.sum_apply {α : Type u_1} {β : Type u_2} {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) (a : α) :
(s.sum (λ (i : ι), f i)) a = s.sum (λ (i : ι), (f i) a)
theorem continuous_map.prod_apply {α : Type u_1} {β : Type u_2} [comm_monoid β] {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) (a : α) :
(s.prod (λ (i : ι), f i)) a = s.prod (λ (i : ι), (f i) a)
@[protected, instance]
def continuous_map.add_group {α : Type u_1} {β : Type u_2} [add_group β]  :
Equations
@[protected, instance]
def continuous_map.group {α : Type u_1} {β : Type u_2} [group β]  :
group C(α, β)
Equations
@[protected, instance]
def continuous_map.comm_group {α : Type u_1} {β : Type u_2} [comm_group β]  :
Equations
• continuous_map.comm_group = continuous_map.comm_group._proof_4 continuous_map.comm_group._proof_5 continuous_map.comm_group._proof_6 continuous_map.comm_group._proof_7 continuous_map.comm_group._proof_8 continuous_map.comm_group._proof_9
@[protected, instance]
def continuous_map.add_comm_group {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.topological_add_group {α : Type u_1} {β : Type u_2}  :
@[protected, instance]
def continuous_map.topological_group {α : Type u_1} {β : Type u_2} [comm_group β]  :

### Ring stucture #

In this section we show that continuous functions valued in a topological semiring `R` inherit the structure of a ring.

def continuous_subsemiring (α : Type u_1) (R : Type u_2) [semiring R]  :
subsemiring (α → R)

The subsemiring of continuous maps `α → β`.

Equations
def continuous_subring (α : Type u_1) (R : Type u_2) [ring R]  :
subring (α → R)

The subring of continuous maps `α → β`.

Equations
@[protected, instance]
def continuous_map.non_unital_non_assoc_semiring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_unital_non_assoc_semiring = continuous_map.non_unital_non_assoc_semiring._proof_1 continuous_map.non_unital_non_assoc_semiring._proof_2 continuous_map.non_unital_non_assoc_semiring._proof_3 continuous_map.non_unital_non_assoc_semiring._proof_4
@[protected, instance]
def continuous_map.non_unital_semiring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_unital_semiring = continuous_map.non_unital_semiring._proof_4 continuous_map.non_unital_semiring._proof_5 continuous_map.non_unital_semiring._proof_6 continuous_map.non_unital_semiring._proof_7
@[protected, instance]
def continuous_map.add_monoid_with_one {α : Type u_1} {β : Type u_2}  :
Equations
@[protected, instance]
def continuous_map.non_assoc_semiring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_assoc_semiring = continuous_map.non_assoc_semiring._proof_4 continuous_map.non_assoc_semiring._proof_5 continuous_map.non_assoc_semiring._proof_6 continuous_map.non_assoc_semiring._proof_7 continuous_map.non_assoc_semiring._proof_8 continuous_map.non_assoc_semiring._proof_9
@[protected, instance]
def continuous_map.semiring {α : Type u_1} {β : Type u_2} [semiring β]  :
Equations
• continuous_map.semiring = continuous_map.semiring._proof_5 continuous_map.semiring._proof_6 continuous_map.semiring._proof_7 continuous_map.semiring._proof_8 continuous_map.semiring._proof_9 continuous_map.semiring._proof_10 continuous_map.semiring._proof_11
@[protected, instance]
def continuous_map.non_unital_non_assoc_ring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_unital_non_assoc_ring = continuous_map.non_unital_non_assoc_ring._proof_5 continuous_map.non_unital_non_assoc_ring._proof_6 continuous_map.non_unital_non_assoc_ring._proof_7 continuous_map.non_unital_non_assoc_ring._proof_8 continuous_map.non_unital_non_assoc_ring._proof_9 continuous_map.non_unital_non_assoc_ring._proof_10 continuous_map.non_unital_non_assoc_ring._proof_11
@[protected, instance]
def continuous_map.non_unital_ring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_unital_ring = continuous_map.non_unital_ring._proof_7 continuous_map.non_unital_ring._proof_8 continuous_map.non_unital_ring._proof_9 continuous_map.non_unital_ring._proof_10 continuous_map.non_unital_ring._proof_11 continuous_map.non_unital_ring._proof_12 continuous_map.non_unital_ring._proof_13
@[protected, instance]
def continuous_map.non_assoc_ring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_assoc_ring = continuous_map.non_assoc_ring._proof_7 continuous_map.non_assoc_ring._proof_8 continuous_map.non_assoc_ring._proof_9 continuous_map.non_assoc_ring._proof_10 continuous_map.non_assoc_ring._proof_11 continuous_map.non_assoc_ring._proof_12 continuous_map.non_assoc_ring._proof_13 continuous_map.non_assoc_ring._proof_14 continuous_map.non_assoc_ring._proof_15 continuous_map.non_assoc_ring._proof_16
@[protected, instance]
def continuous_map.ring {α : Type u_1} {β : Type u_2} [ring β]  :
ring C(α, β)
Equations
• continuous_map.ring = continuous_map.ring._proof_8 continuous_map.ring._proof_9 continuous_map.ring._proof_10 continuous_map.ring._proof_11 continuous_map.ring._proof_12 continuous_map.ring._proof_13 continuous_map.ring._proof_14 continuous_map.ring._proof_15 continuous_map.ring._proof_16 continuous_map.ring._proof_17 continuous_map.ring._proof_18
@[protected, instance]
def continuous_map.non_unital_comm_semiring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_unital_comm_semiring = continuous_map.non_unital_comm_semiring._proof_4 continuous_map.non_unital_comm_semiring._proof_5 continuous_map.non_unital_comm_semiring._proof_6 continuous_map.non_unital_comm_semiring._proof_7
@[protected, instance]
def continuous_map.comm_semiring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.comm_semiring = continuous_map.comm_semiring._proof_5 continuous_map.comm_semiring._proof_6 continuous_map.comm_semiring._proof_7 continuous_map.comm_semiring._proof_8 continuous_map.comm_semiring._proof_9 continuous_map.comm_semiring._proof_10 continuous_map.comm_semiring._proof_11
@[protected, instance]
def continuous_map.non_unital_comm_ring {α : Type u_1} {β : Type u_2}  :
Equations
• continuous_map.non_unital_comm_ring = continuous_map.non_unital_comm_ring._proof_7 continuous_map.non_unital_comm_ring._proof_8 continuous_map.non_unital_comm_ring._proof_9 continuous_map.non_unital_comm_ring._proof_10 continuous_map.non_unital_comm_ring._proof_11 continuous_map.non_unital_comm_ring._proof_12 continuous_map.non_unital_comm_ring._proof_13
@[protected, instance]
def continuous_map.comm_ring {α : Type u_1} {β : Type u_2} [comm_ring β]  :
Equations
• continuous_map.comm_ring = continuous_map.comm_ring._proof_8 continuous_map.comm_ring._proof_9 continuous_map.comm_ring._proof_10 continuous_map.comm_ring._proof_11 continuous_map.comm_ring._proof_12 continuous_map.comm_ring._proof_13 continuous_map.comm_ring._proof_14 continuous_map.comm_ring._proof_15 continuous_map.comm_ring._proof_16 continuous_map.comm_ring._proof_17 continuous_map.comm_ring._proof_18
@[protected]
def ring_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [semiring β] [semiring γ] (g : β →+* γ) (hg : continuous g) :
C(α, β) →+* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological semirings, as a `ring_hom`. Similar to `ring_hom.comp_left`.

Equations
@[simp]
theorem ring_hom.comp_left_continuous_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [semiring β] [semiring γ] (g : β →+* γ) (hg : continuous g) (ᾰ : C(α, β)) :
hg) =
@[simp]
theorem continuous_map.coe_fn_ring_hom_apply {α : Type u_1} {β : Type u_2} [ring β] (x : C(α, β)) (ᾰ : α) :
def continuous_map.coe_fn_ring_hom {α : Type u_1} {β : Type u_2} [ring β]  :
C(α, β) →+* α → β

Coercion to a function as a `ring_hom`.

Equations

### Semiodule stucture #

In this section we show that continuous functions valued in a topological module `M` over a topological semiring `R` inherit the structure of a module.

def continuous_submodule (α : Type u_1) (R : Type u_2) [semiring R] (M : Type u_3) [ M]  :
(α → M)

The `R`-submodule of continuous maps `α → M`.

Equations
@[protected, instance]
def continuous_map.has_smul {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M]  :
C(α, M)
Equations
@[protected, instance]
def continuous_map.has_vadd {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M]  :
C(α, M)
Equations
@[protected, instance]
def continuous_map.has_continuous_const_smul {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M]  :
@[protected, instance]
def continuous_map.has_continuous_const_vadd {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M]  :
@[protected, instance]
def continuous_map.has_continuous_vadd {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] [ M] :
@[protected, instance]
def continuous_map.has_continuous_smul {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] [ M] :
@[simp, norm_cast]
theorem continuous_map.coe_smul {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] (c : R) (f : C(α, M)) :
(c f) = c f
@[simp]
theorem continuous_map.coe_vadd {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] (c : R) (f : C(α, M)) :
(c +ᵥ f) = c +ᵥ f
theorem continuous_map.vadd_apply {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] (c : R) (f : C(α, M)) (a : α) :
(c +ᵥ f) a = c +ᵥ f a
theorem continuous_map.smul_apply {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] (c : R) (f : C(α, M)) (a : α) :
(c f) a = c f a
@[simp]
theorem continuous_map.smul_comp {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_5} [ M] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r f).comp g = r f.comp g
@[simp]
theorem continuous_map.vadd_comp {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_5} [ M] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r +ᵥ f).comp g = r +ᵥ f.comp g
@[protected, instance]
def continuous_map.vadd_comm_class {α : Type u_1} {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [ M] [has_vadd R₁ M] [ R₁ M] :
R₁ C(α, M)
@[protected, instance]
def continuous_map.smul_comm_class {α : Type u_1} {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [ M] [has_smul R₁ M] [ R₁ M] :
R₁ C(α, M)
@[protected, instance]
def continuous_map.is_scalar_tower {α : Type u_1} {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [ M] [has_smul R₁ M] [ R₁] [ R₁ M] :
R₁ C(α, M)
@[protected, instance]
def continuous_map.is_central_scalar {α : Type u_1} {R : Type u_3} {M : Type u_5} [ M] [ M] [ M] :
@[protected, instance]
def continuous_map.mul_action {α : Type u_1} {R : Type u_3} {M : Type u_5} [monoid R] [ M]  :
C(α, M)
Equations
@[protected, instance]
def continuous_map.distrib_mul_action {α : Type u_1} {R : Type u_3} {M : Type u_5} [monoid R] [add_monoid M] [ M]  :
Equations
@[protected, instance]
def continuous_map.module {α : Type u_1} {R : Type u_3} {M : Type u_5} [semiring R] [ M]  :
C(α, M)
Equations
@[simp]
theorem continuous_linear_map.comp_left_continuous_apply (R : Type u_3) {M : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (α : Type u_1) (g : M →L[R] M₂) (ᾰ : C(α, M)) :
@[protected]
def continuous_linear_map.comp_left_continuous (R : Type u_3) {M : Type u_5} {M₂ : Type u_6} [semiring R] [add_comm_monoid M₂] [ M] [ M₂] (α : Type u_1) (g : M →L[R] M₂) :
C(α, M) →ₗ[R] C(α, M₂)

Composition on the left by a continuous linear map, as a `linear_map`. Similar to `linear_map.comp_left`.

Equations
@[simp]
theorem continuous_map.coe_fn_linear_map_apply {α : Type u_1} (R : Type u_3) {M : Type u_5} [semiring R] [ M] (x : C(α, M)) (ᾰ : α) :
= x ᾰ
def continuous_map.coe_fn_linear_map {α : Type u_1} (R : Type u_3) {M : Type u_5} [semiring R] [ M]  :
C(α, M) →ₗ[R] α → M

Coercion to a function as a `linear_map`.

Equations

### Algebra structure #

In this section we show that continuous functions valued in a topological algebra `A` over a ring `R` inherit the structure of an algebra. Note that the hypothesis that `A` is a topological algebra is obtained by requiring that `A` be both a `has_continuous_smul` and a `topological_semiring`.

def continuous_subalgebra {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A]  :
(α → A)

The `R`-subalgebra of continuous maps `α → A`.

Equations
def continuous_map.C {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A]  :
R →+* C(α, A)

Continuous constant functions as a `ring_hom`.

Equations
@[simp]
theorem continuous_map.C_apply {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] (r : R) (a : α) :
a = A) r
@[protected, instance]
def continuous_map.algebra {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A]  :
C(α, A)
Equations
@[protected]
def alg_hom.comp_left_continuous (R : Type u_2) {A : Type u_3} [semiring A] [ A] {A₂ : Type u_4} [semiring A₂] [ A₂] {α : Type u_1} (g : A →ₐ[R] A₂) (hg : continuous g) :
C(α, A) →ₐ[R] C(α, A₂)

Composition on the left by a (continuous) homomorphism of topological `R`-algebras, as an `alg_hom`. Similar to `alg_hom.comp_left`.

Equations
@[simp]
theorem alg_hom.comp_left_continuous_apply (R : Type u_2) {A : Type u_3} [semiring A] [ A] {A₂ : Type u_4} [semiring A₂] [ A₂] {α : Type u_1} (g : A →ₐ[R] A₂) (hg : continuous g) (ᾰ : C(α, A)) :
hg) =
def continuous_map.coe_fn_alg_hom {α : Type u_1} (R : Type u_2) {A : Type u_3} [semiring A] [ A]  :
C(α, A) →ₐ[R] α → A

Coercion to a function as an `alg_hom`.

Equations
@[simp]
theorem continuous_map.coe_fn_alg_hom_apply {α : Type u_1} (R : Type u_2) {A : Type u_3} [semiring A] [ A] (x : C(α, A)) (ᾰ : α) :
= x ᾰ
@[reducible]
def subalgebra.separates_points {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] (s : C(α, A)) :
Prop

A version of `separates_points` for subalgebras of the continuous functions, used for stating the Stone-Weierstrass theorem.

theorem subalgebra.separates_points_monotone {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A]  :
monotone (λ (s : C(α, A)), s.separates_points)
@[simp]
theorem algebra_map_apply {α : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] (k : R) (a : α) :
( C(α, A)) k) a = k 1
def set.separates_points_strongly {α : Type u_1} {𝕜 : Type u_5} (s : set C(α, 𝕜)) :
Prop

A set of continuous maps "separates points strongly" if for each pair of distinct points there is a function with specified values on them.

We give a slightly unusual formulation, where the specified values are given by some function `v`, and we ask `f x = v x ∧ f y = v y`. This avoids needing a hypothesis `x ≠ y`.

In fact, this definition would work perfectly well for a set of non-continuous functions, but as the only current use case is in the Stone-Weierstrass theorem, writing it this way avoids having to deal with casts inside the set. (This may need to change if we do Stone-Weierstrass on non-compact spaces, where the functions would be continuous functions vanishing at infinity.)

Equations
theorem subalgebra.separates_points.strongly {α : Type u_1} {𝕜 : Type u_5} [field 𝕜] {s : C(α, 𝕜)} (h : s.separates_points) :

Working in continuous functions into a topological field, a subalgebra of functions that separates points also separates points strongly.

By the hypothesis, we can find a function `f` so `f x ≠ f y`. By an affine transformation in the field we can arrange so that `f x = a` and `f x = b`.

theorem continuous_map.subsingleton_subalgebra (α : Type u_1) (R : Type u_2) [subsingleton α] :

### Structure as module over scalar functions #

If `M` is a module over `R`, then we show that the space of continuous functions from `α` to `M` is naturally a module over the ring of continuous functions from `α` to `R`.

@[protected, instance]
def continuous_map.has_smul' {α : Type u_1} {R : Type u_2} [semiring R] {M : Type u_3} [ M] [ M] :
Equations
@[protected, instance]
def continuous_map.module' {α : Type u_1} (R : Type u_2) [ring R] (M : Type u_3) [ M] [ M] :
module C(α, R) C(α, M)
Equations

We now provide formulas for `f ⊓ g` and `f ⊔ g`, where `f g : C(α, β)`, in terms of `continuous_map.abs`.

theorem min_eq_half_add_sub_abs_sub {R : Type u_1} {x y : R} :
= 2⁻¹ * (x + y - |x - y|)
= 2⁻¹ * (x + y + |x - y|)
theorem continuous_map.inf_eq {α : Type u_1} {β : Type u_2} (f g : C(α, β)) :
f g = 2⁻¹ (f + g - |f - g|)
theorem continuous_map.sup_eq {α : Type u_1} {β : Type u_2} (f g : C(α, β)) :
f g = 2⁻¹ (f + g + |f - g|)

### Star structure #

If `β` has a continuous star operation, we put a star structure on `C(α, β)` by using the star operation pointwise.

If `β` is a ⋆-ring, then `C(α, β)` inherits a ⋆-ring structure.

If `β` is a ⋆-ring and a ⋆-module over `R`, then the space of continuous functions from `α` to `β` is a ⋆-module over `R`.

@[protected, instance]
def continuous_map.has_star {α : Type u_2} {β : Type u_3} [has_star β]  :
Equations
@[simp]
theorem continuous_map.coe_star {α : Type u_2} {β : Type u_3} [has_star β] (f : C(α, β)) :
@[simp]
theorem continuous_map.star_apply {α : Type u_2} {β : Type u_3} [has_star β] (f : C(α, β)) (x : α) :
@[protected, instance]
def continuous_map.has_involutive_star {α : Type u_2} {β : Type u_3}  :
Equations
@[protected, instance]
def continuous_map.star_add_monoid {α : Type u_2} {β : Type u_3} [add_monoid β]  :
Equations
@[protected, instance]
def continuous_map.star_semigroup {α : Type u_2} {β : Type u_3} [semigroup β]  :
Equations
@[protected, instance]
def continuous_map.star_ring {α : Type u_2} {β : Type u_3} [star_ring β]  :
Equations
@[protected, instance]
def continuous_map.star_module {R : Type u_1} {α : Type u_2} {β : Type u_3} [has_star R] [has_star β] [ β] [ β]  :
C(α, β)