Documentation

Mathlib.Topology.ContinuousMap.Algebra

Algebraic structures over continuous functions #

In this file we define instances of algebraic structures over the type ContinuousMap α β (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 continuousSubgroup α β 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 continuousSubgroup α β), one should use C(α, β) with the appropriate instance of the structure.

instance ContinuousFunctions.instCoeFunElemForallSetOfContinuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] :
CoeFun {f : αβ | Continuous f} fun (x : {f : αβ | Continuous f}) => αβ
Equations
  • ContinuousFunctions.instCoeFunElemForallSetOfContinuous = { coe := Subtype.val }

mul and add #

instance ContinuousMap.instAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] :
Add C(α, β)
Equations
  • ContinuousMap.instAdd = { add := fun (f g : C(α, β)) => { toFun := f + g, continuous_toFun := } }
theorem ContinuousMap.instAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
Continuous ((fun (p : β × β) => p.1 + p.2) fun (x : α) => (f x, g x))
instance ContinuousMap.instMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] :
Mul C(α, β)
Equations
  • ContinuousMap.instMul = { mul := fun (f g : C(α, β)) => { toFun := f * g, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_add {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
(f + g) = f + g
@[simp]
theorem ContinuousMap.coe_mul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] (f : C(α, β)) (g : C(α, β)) :
(f * g) = f * g
@[simp]
theorem ContinuousMap.add_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Add β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f + g) x = f x + g x
@[simp]
theorem ContinuousMap.mul_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f * g) x = f x * g x
@[simp]
theorem ContinuousMap.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f₁ : C(β, γ)) (f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
@[simp]
theorem ContinuousMap.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f₁ : C(β, γ)) (f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ * f₂).comp g = f₁.comp g * f₂.comp g

one #

instance ContinuousMap.instZero {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] :
Zero C(α, β)
Equations
instance ContinuousMap.instOne {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] :
One C(α, β)
Equations
@[simp]
theorem ContinuousMap.coe_zero {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] :
0 = 0
@[simp]
theorem ContinuousMap.coe_one {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] :
1 = 1
@[simp]
theorem ContinuousMap.zero_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (x : α) :
0 x = 0
@[simp]
theorem ContinuousMap.one_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] (x : α) :
1 x = 1
@[simp]
theorem ContinuousMap.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Zero γ] (g : C(α, β)) :
@[simp]
theorem ContinuousMap.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [One γ] (g : C(α, β)) :

Nat.cast #

instance ContinuousMap.instNatCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] :
Equations
@[simp]
theorem ContinuousMap.coe_natCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ) :
n = n
@[deprecated ContinuousMap.coe_natCast]
theorem ContinuousMap.coe_nat_cast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ) :
n = n

Alias of ContinuousMap.coe_natCast.

@[simp]
theorem ContinuousMap.natCast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ) (x : α) :
n x = n
@[deprecated ContinuousMap.natCast_apply]
theorem ContinuousMap.nat_cast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NatCast β] (n : ) (x : α) :
n x = n

Alias of ContinuousMap.natCast_apply.

Int.cast #

instance ContinuousMap.instIntCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] :
Equations
@[simp]
theorem ContinuousMap.coe_intCast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ) :
n = n
@[deprecated ContinuousMap.coe_intCast]
theorem ContinuousMap.coe_int_cast {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ) :
n = n

Alias of ContinuousMap.coe_intCast.

@[simp]
theorem ContinuousMap.intCast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ) (x : α) :
n x = n
@[deprecated ContinuousMap.intCast_apply]
theorem ContinuousMap.int_cast_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [IntCast β] (n : ) (x : α) :
n x = n

Alias of ContinuousMap.intCast_apply.

nsmul and pow #

instance ContinuousMap.instNSMul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] :
Equations
  • ContinuousMap.instNSMul = { smul := fun (n : ) (f : C(α, β)) => { toFun := n f, continuous_toFun := } }
instance ContinuousMap.instPow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] :
Pow C(α, β)
Equations
  • ContinuousMap.instPow = { pow := fun (f : C(α, β)) (n : ) => { toFun := f ^ n, continuous_toFun := } }
theorem ContinuousMap.coe_nsmul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (n : ) (f : C(α, β)) :
(n f) = n f
@[simp]
theorem ContinuousMap.coe_pow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : ) :
(f ^ n) = f ^ n
theorem ContinuousMap.nsmul_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (n : ) (x : α) :
(n f) x = n f x
@[simp]
theorem ContinuousMap.pow_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] (f : C(α, β)) (n : ) (x : α) :
(f ^ n) x = f x ^ n
theorem ContinuousMap.nsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(n f).comp g = n f.comp g
@[simp]
theorem ContinuousMap.pow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(f ^ n).comp g = f.comp g ^ n

inv and neg #

Equations
  • ContinuousMap.instNegOfContinuousNeg = { neg := fun (f : C(α, β)) => { toFun := -f, continuous_toFun := } }
theorem ContinuousMap.instNegOfContinuousNeg.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) :
Continuous fun (x : α) => -f x
Equations
  • ContinuousMap.instInvOfContinuousInv = { inv := fun (f : C(α, β)) => { toFun := (⇑f)⁻¹, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_neg {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) :
(-f) = -f
@[simp]
theorem ContinuousMap.coe_inv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inv β] [ContinuousInv β] (f : C(α, β)) :
f⁻¹ = (⇑f)⁻¹
@[simp]
theorem ContinuousMap.neg_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Neg β] [ContinuousNeg β] (f : C(α, β)) (x : α) :
(-f) x = -f x
@[simp]
theorem ContinuousMap.inv_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Inv β] [ContinuousInv β] (f : C(α, β)) (x : α) :
f⁻¹ x = (f x)⁻¹
@[simp]
theorem ContinuousMap.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Neg γ] [ContinuousNeg γ] (f : C(β, γ)) (g : C(α, β)) :
(-f).comp g = -f.comp g
@[simp]
theorem ContinuousMap.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Inv γ] [ContinuousInv γ] (f : C(β, γ)) (g : C(α, β)) :
f⁻¹.comp g = (f.comp g)⁻¹

div and sub #

theorem ContinuousMap.instSubOfContinuousSub.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] (f : C(α, β)) (g : C(α, β)) :
Continuous fun (x : α) => f x - g x
Equations
  • ContinuousMap.instSubOfContinuousSub = { sub := fun (f g : C(α, β)) => { toFun := f - g, continuous_toFun := } }
Equations
  • ContinuousMap.instDivOfContinuousDiv = { div := fun (f g : C(α, β)) => { toFun := f / g, continuous_toFun := } }
@[simp]
theorem ContinuousMap.coe_sub {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] (f : C(α, β)) (g : C(α, β)) :
(f - g) = f - g
@[simp]
theorem ContinuousMap.coe_div {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Div β] [ContinuousDiv β] (f : C(α, β)) (g : C(α, β)) :
(f / g) = f / g
@[simp]
theorem ContinuousMap.sub_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Sub β] [ContinuousSub β] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f - g) x = f x - g x
@[simp]
theorem ContinuousMap.div_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Div β] [ContinuousDiv β] (f : C(α, β)) (g : C(α, β)) (x : α) :
(f / g) x = f x / g x
@[simp]
theorem ContinuousMap.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Sub γ] [ContinuousSub γ] (f : C(β, γ)) (g : C(β, γ)) (h : C(α, β)) :
(f - g).comp h = f.comp h - g.comp h
@[simp]
theorem ContinuousMap.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Div γ] [ContinuousDiv γ] (f : C(β, γ)) (g : C(β, γ)) (h : C(α, β)) :
(f / g).comp h = f.comp h / g.comp h

zpow and zsmul #

Equations
  • ContinuousMap.instZSMul = { smul := fun (z : ) (f : C(α, β)) => { toFun := z f, continuous_toFun := } }
instance ContinuousMap.instZPow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] :
Pow C(α, β)
Equations
  • ContinuousMap.instZPow = { pow := fun (f : C(α, β)) (z : ) => { toFun := f ^ z, continuous_toFun := } }
theorem ContinuousMap.coe_zsmul {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (z : ) (f : C(α, β)) :
(z f) = z f
@[simp]
theorem ContinuousMap.coe_zpow {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] (f : C(α, β)) (z : ) :
(f ^ z) = f ^ z
theorem ContinuousMap.zsmul_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (z : ) (x : α) :
(z f) x = z f x
@[simp]
theorem ContinuousMap.zpow_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] (f : C(α, β)) (z : ) (x : α) :
(f ^ z) x = f x ^ z
theorem ContinuousMap.zsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [AddGroup γ] [TopologicalAddGroup γ] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(z f).comp g = z f.comp g
@[simp]
theorem ContinuousMap.zpow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Group γ] [TopologicalGroup γ] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(f ^ z).comp g = f.comp g ^ z

Group structure #

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

def continuousAddSubmonoid (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] :
AddSubmonoid (αβ)

The AddSubmonoid of continuous maps α → β.

Equations
Instances For
    theorem continuousAddSubmonoid.proof_1 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] :
    ∀ {a b : αβ}, a {f : αβ | Continuous f}b {f : αβ | Continuous f}Continuous fun (x : α) => a x + b x
    theorem continuousAddSubmonoid.proof_2 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] :
    Continuous fun (x : α) => 0
    def continuousSubmonoid (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [MulOneClass β] [ContinuousMul β] :
    Submonoid (αβ)

    The Submonoid of continuous maps α → β.

    Equations
    Instances For
      def continuousAddSubgroup (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :
      AddSubgroup (αβ)

      The AddSubgroup of continuous maps α → β.

      Equations
      Instances For
        theorem continuousAddSubgroup.proof_1 (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] :
        ∀ {x : αβ}, x (continuousAddSubmonoid α β).carrierContinuous fun (x_1 : α) => -x x_1
        def continuousSubgroup (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] [Group β] [TopologicalGroup β] :
        Subgroup (αβ)

        The subgroup of continuous maps α → β.

        Equations
        Instances For
          theorem ContinuousMap.instAddSemigroupOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddSemigroup β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
          (f + g) = f + g
          Equations
          Equations
          Equations
          theorem ContinuousMap.instAddCommSemigroupOfContinuousAdd.proof_1 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommSemigroup β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
          (f + g) = f + g
          Equations
          Equations
          theorem ContinuousMap.instAddZeroClassOfContinuousAdd.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
          (f + g) = f + g
          Equations
          Equations
          Equations
          theorem ContinuousMap.instAddMonoidOfContinuousAdd.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
          (f + g) = f + g
          Equations
          Equations
          Equations
          theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
          (f + g) = f + g
          Equations
          theorem ContinuousMap.instAddCommMonoidOfContinuousAdd.proof_3 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] (f : C(α, β)) (n : ) :
          (n f) = n f
          Equations
          Equations
          theorem ContinuousMap.coeFnAddMonoidHom.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (g : C(α, β)) :
          (f + g) = f + g
          def ContinuousMap.coeFnAddMonoidHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] :
          C(α, β) →+ αβ

          Coercion to a function as an AddMonoidHom. Similar to AddMonoidHom.coeFn.

          Equations
          • ContinuousMap.coeFnAddMonoidHom = { toFun := fun (f : C(α, β)) => f, map_zero' := , map_add' := }
          Instances For
            @[simp]
            theorem ContinuousMap.coeFnMonoidHom_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] (f : C(α, β)) (a : α) :
            ContinuousMap.coeFnMonoidHom f a = f a
            @[simp]
            theorem ContinuousMap.coeFnAddMonoidHom_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (f : C(α, β)) (a : α) :
            ContinuousMap.coeFnAddMonoidHom f a = f a
            def ContinuousMap.coeFnMonoidHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Monoid β] [ContinuousMul β] :
            C(α, β) →* αβ

            Coercion to a function as a MonoidHom. Similar to MonoidHom.coeFn.

            Equations
            • ContinuousMap.coeFnMonoidHom = { toFun := fun (f : C(α, β)) => f, map_one' := , map_mul' := }
            Instances For
              theorem AddMonoidHom.compLeftContinuous.proof_1 (α : Type u_1) {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_2} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous g) :
              (fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f) 0 = 0
              theorem AddMonoidHom.compLeftContinuous.proof_2 (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous g) :
              ∀ (x x_1 : C(α, β)), { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := }.toFun (x + x_1) = { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := }.toFun x + { toFun := fun (f : C(α, β)) => { toFun := g, continuous_toFun := hg }.comp f, map_zero' := }.toFun x_1
              def AddMonoidHom.compLeftContinuous (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous g) :
              C(α, β) →+ C(α, γ)

              Composition on the left by a (continuous) homomorphism of topological AddMonoids, as an AddMonoidHom. Similar to AddMonoidHom.comp_left.

              Equations
              Instances For
                @[simp]
                theorem MonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [Monoid β] [ContinuousMul β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (g : β →* γ) (hg : Continuous g) (f : C(α, β)) :
                (MonoidHom.compLeftContinuous α g hg) f = { toFun := g, continuous_toFun := hg }.comp f
                @[simp]
                theorem AddMonoidHom.compLeftContinuous_apply (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddMonoid β] [ContinuousAdd β] [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (g : β →+ γ) (hg : Continuous g) (f : C(α, β)) :
                (AddMonoidHom.compLeftContinuous α g hg) f = { toFun := g, continuous_toFun := hg }.comp f
                def MonoidHom.compLeftContinuous (α : Type u_1) {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [Monoid β] [ContinuousMul β] [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (g : β →* γ) (hg : Continuous g) :
                C(α, β) →* C(α, γ)

                Composition on the left by a (continuous) homomorphism of topological monoids, as a MonoidHom. Similar to MonoidHom.compLeft.

                Equations
                Instances For
                  def ContinuousMap.compAddMonoidHom' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [AddZeroClass γ] [ContinuousAdd γ] (g : C(α, β)) :
                  C(β, γ) →+ C(α, γ)

                  Composition on the right as an AddMonoidHom. Similar to AddMonoidHom.compHom'.

                  Equations
                  • g.compAddMonoidHom' = { toFun := fun (f : C(β, γ)) => f.comp g, map_zero' := , map_add' := }
                  Instances For
                    theorem ContinuousMap.compAddMonoidHom'.proof_2 {α : Type u_3} {β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_2} [TopologicalSpace γ] [AddZeroClass γ] [ContinuousAdd γ] (g : C(α, β)) (f₁ : C(β, γ)) (f₂ : C(β, γ)) :
                    (f₁ + f₂).comp g = f₁.comp g + f₂.comp g
                    @[simp]
                    theorem ContinuousMap.compMonoidHom'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [MulOneClass γ] [ContinuousMul γ] (g : C(α, β)) (f : C(β, γ)) :
                    g.compMonoidHom' f = f.comp g
                    @[simp]
                    theorem ContinuousMap.compAddMonoidHom'_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [AddZeroClass γ] [ContinuousAdd γ] (g : C(α, β)) (f : C(β, γ)) :
                    g.compAddMonoidHom' f = f.comp g
                    def ContinuousMap.compMonoidHom' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] [MulOneClass γ] [ContinuousMul γ] (g : C(α, β)) :
                    C(β, γ) →* C(α, γ)

                    Composition on the right as a MonoidHom. Similar to MonoidHom.compHom'.

                    Equations
                    • g.compMonoidHom' = { toFun := fun (f : C(β, γ)) => f.comp g, map_one' := , map_mul' := }
                    Instances For
                      @[simp]
                      theorem ContinuousMap.coe_sum {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ιC(α, β)) :
                      (∑ is, f i) = is, (f i)
                      @[simp]
                      theorem ContinuousMap.coe_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] {ι : Type u_3} (s : Finset ι) (f : ιC(α, β)) :
                      (∏ is, f i) = is, (f i)
                      theorem ContinuousMap.sum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ιC(α, β)) (a : α) :
                      (∑ is, f i) a = is, (f i) a
                      theorem ContinuousMap.prod_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [CommMonoid β] [ContinuousMul β] {ι : Type u_3} (s : Finset ι) (f : ιC(α, β)) (a : α) :
                      (∏ is, f i) a = is, (f i) a
                      theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_5 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (n : ) :
                      (n f) = n f
                      Equations
                      theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_4 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) :
                      (f - g) = f - g
                      theorem ContinuousMap.instAddGroupOfTopologicalAddGroup.proof_2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) :
                      (f + g) = f + g
                      Equations
                      theorem ContinuousMap.instAddCommGroupContinuousMap.proof_7 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) :
                      (f - g) = f - g
                      theorem ContinuousMap.instAddCommGroupContinuousMap.proof_5 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (g : C(α, β)) :
                      (f + g) = f + g
                      theorem ContinuousMap.instAddCommGroupContinuousMap.proof_8 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (n : ) :
                      (n f) = n f
                      theorem ContinuousMap.instAddCommGroupContinuousMap.proof_9 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommGroup β] [TopologicalAddGroup β] (f : C(α, β)) (z : ) :
                      (z f) = z f
                      Equations
                      Equations
                      theorem ContinuousMap.hasSum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [AddCommMonoid β] [ContinuousAdd β] {f : γC(α, β)} {g : C(α, β)} (hf : HasSum f g) (x : α) :
                      HasSum (fun (i : γ) => (f i) x) (g x)

                      If α is locally compact, and an infinite sum of functions in C(α, β) converges to g (for the compact-open topology), then the pointwise sum converges to g x for all x ∈ α.

                      theorem ContinuousMap.summable_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γC(α, β)} (hf : Summable f) (x : α) :
                      Summable fun (i : γ) => (f i) x
                      theorem ContinuousMap.tsum_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type u_3} {f : γC(α, β)} (hf : Summable f) (x : α) :
                      ∑' (i : γ), (f i) x = (∑' (i : γ), f i) x

                      Ring structure #

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

                      The subsemiring of continuous maps α → β.

                      Equations
                      Instances For
                        def continuousSubring (α : Type u_1) (R : Type u_2) [TopologicalSpace α] [TopologicalSpace R] [Ring R] [TopologicalRing R] :
                        Subring (αR)

                        The subring of continuous maps α → β.

                        Equations
                        Instances For
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          instance ContinuousMap.instRing {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Ring β] [TopologicalRing β] :
                          Ring C(α, β)
                          Equations
                          Equations
                          Equations
                          Equations
                          Equations
                          @[simp]
                          theorem RingHom.compLeftContinuous_apply_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] [TopologicalSpace γ] [Semiring γ] [TopologicalSemiring γ] (g : β →+* γ) (hg : Continuous g) (f : C(α, β)) :
                          ∀ (a : α), ((RingHom.compLeftContinuous α g hg) f) a = g (f a)
                          def RingHom.compLeftContinuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] [TopologicalSpace γ] [Semiring γ] [TopologicalSemiring γ] (g : β →+* γ) (hg : Continuous g) :
                          C(α, β) →+* C(α, γ)

                          Composition on the left by a (continuous) homomorphism of topological semirings, as a RingHom. Similar to RingHom.compLeft.

                          Equations
                          Instances For
                            @[simp]
                            theorem ContinuousMap.coeFnRingHom_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] (f : C(α, β)) (a : α) :
                            ContinuousMap.coeFnRingHom f a = f a
                            def ContinuousMap.coeFnRingHom {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [TopologicalSemiring β] :
                            C(α, β) →+* αβ

                            Coercion to a function as a RingHom.

                            Equations
                            • ContinuousMap.coeFnRingHom = { toMonoidHom := ContinuousMap.coeFnMonoidHom, map_zero' := , map_add' := }
                            Instances For

                              Module structure #

                              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 continuousSubmodule (α : Type u_1) [TopologicalSpace α] (R : Type u_2) [Semiring R] (M : Type u_3) [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousConstSMul R M] [TopologicalAddGroup M] :
                              Submodule R (αM)

                              The R-submodule of continuous maps α → M.

                              Equations
                              Instances For
                                theorem ContinuousMap.instVAdd.proof_1 {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_2} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (r : R) (f : C(α, M)) :
                                Continuous fun (x : α) => r +ᵥ f x
                                instance ContinuousMap.instVAdd {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] :
                                VAdd R C(α, M)
                                Equations
                                • ContinuousMap.instVAdd = { vadd := fun (r : R) (f : C(α, M)) => { toFun := r +ᵥ f, continuous_toFun := } }
                                instance ContinuousMap.instSMul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] :
                                SMul R C(α, M)
                                Equations
                                • ContinuousMap.instSMul = { smul := fun (r : R) (f : C(α, M)) => { toFun := r f, continuous_toFun := } }
                                @[simp]
                                theorem ContinuousMap.coe_vadd {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (c : R) (f : C(α, M)) :
                                (c +ᵥ f) = c +ᵥ f
                                @[simp]
                                theorem ContinuousMap.coe_smul {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) :
                                (c f) = c f
                                theorem ContinuousMap.vadd_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (c : R) (f : C(α, M)) (a : α) :
                                (c +ᵥ f) a = c +ᵥ f a
                                theorem ContinuousMap.smul_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] (c : R) (f : C(α, M)) (a : α) :
                                (c f) a = c f a
                                @[simp]
                                theorem ContinuousMap.vadd_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
                                (r +ᵥ f).comp g = r +ᵥ f.comp g
                                @[simp]
                                theorem ContinuousMap.smul_comp {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
                                (r f).comp g = r f.comp g
                                instance ContinuousMap.instVAddCommClass {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [TopologicalSpace M] [VAdd R M] [ContinuousConstVAdd R M] [VAdd R₁ M] [ContinuousConstVAdd R₁ M] [VAddCommClass R R₁ M] :
                                VAddCommClass R R₁ C(α, M)
                                Equations
                                • =
                                instance ContinuousMap.instSMulCommClass {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [SMul R₁ M] [ContinuousConstSMul R₁ M] [SMulCommClass R R₁ M] :
                                SMulCommClass R R₁ C(α, M)
                                Equations
                                • =
                                instance ContinuousMap.instIsScalarTower {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [TopologicalSpace M] [SMul R M] [ContinuousConstSMul R M] [SMul R₁ M] [ContinuousConstSMul R₁ M] [SMul R R₁] [IsScalarTower R R₁ M] :
                                IsScalarTower R R₁ C(α, M)
                                Equations
                                • =
                                Equations
                                • =
                                Equations
                                Equations
                                instance ContinuousMap.module {α : Type u_1} [TopologicalSpace α] {R : Type u_3} {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] :
                                Module R C(α, M)
                                Equations
                                @[simp]
                                theorem ContinuousLinearMap.compLeftContinuous_apply (R : Type u_3) {M : Type u_5} [TopologicalSpace M] {M₂ : Type u_6} [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M₂] [Module R M₂] [ContinuousConstSMul R M₂] (α : Type u_7) [TopologicalSpace α] (g : M →L[R] M₂) :
                                ∀ (a : C(α, M)), (ContinuousLinearMap.compLeftContinuous R α g) a = (↑(AddMonoidHom.compLeftContinuous α (↑g).toAddMonoidHom )).toFun a
                                def ContinuousLinearMap.compLeftContinuous (R : Type u_3) {M : Type u_5} [TopologicalSpace M] {M₂ : Type u_6} [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M₂] [Module R M₂] [ContinuousConstSMul R M₂] (α : Type u_7) [TopologicalSpace α] (g : M →L[R] M₂) :
                                C(α, M) →ₗ[R] C(α, M₂)

                                Composition on the left by a continuous linear map, as a LinearMap. Similar to LinearMap.compLeft.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem ContinuousMap.coeFnLinearMap_apply {α : Type u_1} [TopologicalSpace α] (R : Type u_3) {M : Type u_5} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] :
                                  ∀ (a : C(α, M)) (a_1 : α), (ContinuousMap.coeFnLinearMap R) a a_1 = (↑ContinuousMap.coeFnAddMonoidHom).toFun a a_1

                                  Coercion to a function as a LinearMap.

                                  Equations
                                  Instances For

                                    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 ContinuousSMul and a TopologicalSemiring.

                                    def continuousSubalgebra {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] :
                                    Subalgebra R (αA)

                                    The R-subalgebra of continuous maps α → A.

                                    Equations
                                    • continuousSubalgebra = { carrier := {f : αA | Continuous f}, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
                                    Instances For
                                      def ContinuousMap.C {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] :
                                      R →+* C(α, A)

                                      Continuous constant functions as a RingHom.

                                      Equations
                                      • ContinuousMap.C = { toFun := fun (c : R) => { toFun := fun (x : α) => (algebraMap R A) c, continuous_toFun := }, map_one' := , map_mul' := , map_zero' := , map_add' := }
                                      Instances For
                                        @[simp]
                                        theorem ContinuousMap.C_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (r : R) (a : α) :
                                        (ContinuousMap.C r) a = (algebraMap R A) r
                                        instance ContinuousMap.algebra {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] :
                                        Equations
                                        • ContinuousMap.algebra = Algebra.mk ContinuousMap.C
                                        @[simp]
                                        theorem AlgHom.compLeftContinuous_apply_apply (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [TopologicalSemiring A₂] {α : Type u_5} [TopologicalSpace α] (g : A →ₐ[R] A₂) (hg : Continuous g) (f : C(α, A)) :
                                        ∀ (a : α), ((AlgHom.compLeftContinuous R g hg) f) a = g (f a)
                                        def AlgHom.compLeftContinuous (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {A₂ : Type u_4} [TopologicalSpace A₂] [Semiring A₂] [Algebra R A₂] [TopologicalSemiring A₂] {α : Type u_5} [TopologicalSpace α] (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 AlgHom. Similar to AlgHom.compLeft.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem ContinuousMap.compRightAlgHom_apply (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (g : C(β, A)) :
                                          (ContinuousMap.compRightAlgHom R A f) g = g.comp f
                                          def ContinuousMap.compRightAlgHom (R : Type u_2) [CommSemiring R] (A : Type u_3) [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) :
                                          C(β, A) →ₐ[R] C(α, A)

                                          Precomposition of functions into a topological semiring by a continuous map is an algebra homomorphism.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem ContinuousMap.coeFnAlgHom_apply {α : Type u_1} [TopologicalSpace α] (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (f : C(α, A)) (a : α) :
                                            def ContinuousMap.coeFnAlgHom {α : Type u_1} [TopologicalSpace α] (R : Type u_2) [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] :
                                            C(α, A) →ₐ[R] αA

                                            Coercion to a function as an AlgHom.

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev Subalgebra.SeparatesPoints {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R C(α, A)) :

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

                                              Equations
                                              • s.SeparatesPoints = ((fun (f : C(α, A)) => f) '' s).SeparatesPoints
                                              Instances For
                                                theorem Subalgebra.separatesPoints_monotone {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] :
                                                Monotone fun (s : Subalgebra R C(α, A)) => s.SeparatesPoints
                                                @[simp]
                                                theorem algebraMap_apply {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [CommSemiring R] {A : Type u_3} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (k : R) (a : α) :
                                                ((algebraMap R C(α, A)) k) a = k 1
                                                def Set.SeparatesPointsStrongly {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_5} [TopologicalSpace 𝕜] (s : Set C(α, 𝕜)) :

                                                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
                                                • s.SeparatesPointsStrongly = ∀ (v : α𝕜) (x y : α), fs, f x = v x f y = v y
                                                Instances For
                                                  theorem Subalgebra.SeparatesPoints.strongly {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [Field 𝕜] [TopologicalRing 𝕜] {s : Subalgebra 𝕜 C(α, 𝕜)} (h : s.SeparatesPoints) :
                                                  (↑s).SeparatesPointsStrongly

                                                  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.

                                                  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.

                                                  instance ContinuousMap.instSMul' {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [Semiring R] [TopologicalSpace R] {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousSMul R M] :
                                                  SMul C(α, R) C(α, M)
                                                  Equations
                                                  • ContinuousMap.instSMul' = { smul := fun (f : C(α, R)) (g : C(α, M)) => { toFun := fun (x : α) => f x g x, continuous_toFun := } }

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

                                                  C(α, β)is a lattice ordered group

                                                  instance ContinuousMap.instCovariantClass_add_le_left {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Add β] [ContinuousAdd β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] :
                                                  CovariantClass C(α, β) C(α, β) (fun (x1 x2 : C(α, β)) => x1 + x2) fun (x1 x2 : C(α, β)) => x1 x2
                                                  Equations
                                                  • =
                                                  instance ContinuousMap.instCovariantClass_mul_le_left {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Mul β] [ContinuousMul β] [CovariantClass β β (fun (x1 x2 : β) => x1 * x2) fun (x1 x2 : β) => x1 x2] :
                                                  CovariantClass C(α, β) C(α, β) (fun (x1 x2 : C(α, β)) => x1 * x2) fun (x1 x2 : C(α, β)) => x1 x2
                                                  Equations
                                                  • =
                                                  instance ContinuousMap.instCovariantClass_add_le_right {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Add β] [ContinuousAdd β] [CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 x2] :
                                                  CovariantClass C(α, β) C(α, β) (Function.swap fun (x1 x2 : C(α, β)) => x1 + x2) fun (x1 x2 : C(α, β)) => x1 x2
                                                  Equations
                                                  • =
                                                  instance ContinuousMap.instCovariantClass_mul_le_right {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [PartialOrder β] [Mul β] [ContinuousMul β] [CovariantClass β β (Function.swap fun (x1 x2 : β) => x1 * x2) fun (x1 x2 : β) => x1 x2] :
                                                  CovariantClass C(α, β) C(α, β) (Function.swap fun (x1 x2 : C(α, β)) => x1 * x2) fun (x1 x2 : C(α, β)) => x1 x2
                                                  Equations
                                                  • =
                                                  @[simp]
                                                  theorem ContinuousMap.coe_abs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) :
                                                  |f| = |f|
                                                  @[simp]
                                                  theorem ContinuousMap.coe_mabs {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [TopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) :
                                                  (mabs f) = mabs f
                                                  @[simp]
                                                  theorem ContinuousMap.abs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) :
                                                  |f| x = |f x|
                                                  @[simp]
                                                  theorem ContinuousMap.mabs_apply {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] [Group β] [TopologicalGroup β] [Lattice β] [TopologicalLattice β] (f : C(α, β)) (x : α) :
                                                  (mabs f) x = mabs (f x)

                                                  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.

                                                  instance ContinuousMap.instStar {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] :
                                                  Star C(α, β)
                                                  Equations
                                                  • ContinuousMap.instStar = { star := fun (f : C(α, β)) => starContinuousMap.comp f }
                                                  @[simp]
                                                  theorem ContinuousMap.coe_star {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) :
                                                  (star f) = star f
                                                  @[simp]
                                                  theorem ContinuousMap.star_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star β] [ContinuousStar β] (f : C(α, β)) (x : α) :
                                                  (star f) x = star (f x)
                                                  Equations
                                                  • =
                                                  Equations
                                                  Equations
                                                  instance ContinuousMap.starMul {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Mul β] [ContinuousMul β] [StarMul β] [ContinuousStar β] :
                                                  Equations
                                                  Equations
                                                  • ContinuousMap.instStarRingOfContinuousStar = StarRing.mk
                                                  instance ContinuousMap.instStarModule {R : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Star R] [Star β] [SMul R β] [StarModule R β] [ContinuousStar β] [ContinuousConstSMul R β] :
                                                  Equations
                                                  • =
                                                  @[simp]
                                                  theorem ContinuousMap.compStarAlgHom'_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) (g : C(Y, A)) :
                                                  (ContinuousMap.compStarAlgHom' 𝕜 A f) g = g.comp f
                                                  def ContinuousMap.compStarAlgHom' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (f : C(X, Y)) :

                                                  The functorial map taking f : C(X, Y) to C(Y, A) →⋆ₐ[𝕜] C(X, A) given by pre-composition with the continuous function f. See ContinuousMap.compMonoidHom' and ContinuousMap.compAddMonoidHom', ContinuousMap.compRightAlgHom for bundlings of pre-composition into a MonoidHom, an AddMonoidHom and an AlgHom, respectively, under suitable assumptions on A.

                                                  Equations
                                                  • ContinuousMap.compStarAlgHom' 𝕜 A f = { toFun := fun (g : C(Y, A)) => g.comp f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := , map_star' := }
                                                  Instances For

                                                    ContinuousMap.compStarAlgHom' sends the identity continuous map to the identity StarAlgHom

                                                    theorem ContinuousMap.compStarAlgHom'_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (𝕜 : Type u_4) [CommSemiring 𝕜] (A : Type u_5) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)) :

                                                    ContinuousMap.compStarAlgHom' is functorial.

                                                    @[simp]
                                                    theorem ContinuousMap.compStarAlgHom_apply (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous φ) (f : C(X, A)) :
                                                    (ContinuousMap.compStarAlgHom X φ ) f = { toFun := φ, continuous_toFun := }.comp f
                                                    def ContinuousMap.compStarAlgHom (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] (φ : A →⋆ₐ[𝕜] B) (hφ : Continuous φ) :

                                                    Post-composition with a continuous star algebra homomorphism is a star algebra homomorphism between spaces of continuous maps.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      ContinuousMap.compStarAlgHom sends the identity StarAlgHom on A to the identity StarAlgHom on C(X, A).

                                                      theorem ContinuousMap.compStarAlgHom_comp (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [TopologicalSpace X] [CommSemiring 𝕜] [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [Star A] [ContinuousStar A] [Algebra 𝕜 A] [TopologicalSpace B] [Semiring B] [TopologicalSemiring B] [Star B] [ContinuousStar B] [Algebra 𝕜 B] [TopologicalSpace C] [Semiring C] [TopologicalSemiring C] [Star C] [ContinuousStar C] [Algebra 𝕜 C] (φ : A →⋆ₐ[𝕜] B) (ψ : B →⋆ₐ[𝕜] C) (hφ : Continuous φ) (hψ : Continuous ψ) :

                                                      ContinuousMap.compStarAlgHom is functorial.

                                                      Summing translates of a function #

                                                      Summing the translates of f by ℤ • p gives a map which is periodic with period p. (This is true without any convergence conditions, since if the sum doesn't converge it is taken to be the zero map, which is periodic.)

                                                      @[simp]
                                                      theorem Homeomorph.compStarAlgEquiv'_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(Y, A)) :
                                                      (Homeomorph.compStarAlgEquiv' 𝕜 A f) a = (ContinuousMap.compStarAlgHom' 𝕜 A f.toContinuousMap) a
                                                      @[simp]
                                                      theorem Homeomorph.compStarAlgEquiv'_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) (a : C(X, A)) :
                                                      (Homeomorph.compStarAlgEquiv' 𝕜 A f).symm a = (ContinuousMap.compStarAlgHom' 𝕜 A f.symm.toContinuousMap) a
                                                      def Homeomorph.compStarAlgEquiv' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (𝕜 : Type u_3) [CommSemiring 𝕜] (A : Type u_4) [TopologicalSpace A] [Semiring A] [TopologicalSemiring A] [StarRing A] [ContinuousStar A] [Algebra 𝕜 A] (f : X ≃ₜ Y) :

                                                      ContinuousMap.compStarAlgHom' as a StarAlgEquiv when the continuous map f is actually a homeomorphism.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        Evaluation as a bundled map #

                                                        @[simp]
                                                        theorem ContinuousMap.evalAlgHom_apply {X : Type u_1} (S : Type u_2) (R : Type u_3) [TopologicalSpace X] [CommSemiring S] [CommSemiring R] [Algebra S R] [TopologicalSpace R] [TopologicalSemiring R] (x : X) (f : C(X, R)) :

                                                        Evaluation of continuous maps at a point, bundled as an algebra homomorphism.

                                                        Equations
                                                        • ContinuousMap.evalAlgHom S R x = { toFun := fun (f : C(X, R)) => f x, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                                                        Instances For
                                                          @[simp]

                                                          Evaluation of continuous maps at a point, bundled as a star algebra homomorphism.

                                                          Equations
                                                          Instances For