Theorems · Theorem · general topology

Continuous.dotProduct

∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Fintype n] [inst_3 : Mul R] [inst_4 : AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R]
  {A B : X → n → R}, Continuous A → Continuous B → Continuous fun x => A x ⬝ᵥ B x

Defined in

Mathlib.Topology.Instances.Matrix

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceFintypeMulAddCommMonoidContinuousAddContinuousMul