Theorems · Definition · general topology

ContinuousMap.prodMul

{X : Type u_5} →
  {Y : Type u_6} →
    {R : Type u_7} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] → [inst_4 : IsTopologicalRing R] → C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)

The natural bilinear map sending f, g to the function (x, y) ↦ f x * g y on X × Y.

Defined in

Mathlib.Topology.UniformSpace.ProdApproximation

Cited by

4 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceCommRingTopologicalSpaceIsTopologicalRing