Continuity of addition on bounded continuous functions

For bounded continuous functions with values in a normed ring, such as the continuous linear endomorphisms of a normed space, instance resolution derives ContinuousAdd (α →ᵇ β) from the topological ring structure. The addition in that instance is the one of the ring, while a space of continuous linear maps out of C(K, α →ᵇ β) is stated with the addition of the additive group, so every declaration mentioning such a space makes the kernel compare the two additions.

The instance below derives the continuity from the additive group, for every seminormed group of values, and is tried first.

@[instance 10000]

instance NavierStokesAndEuler.BoundedContinuousFunctionShortcut.instContinuousAdd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [SeminormedAddCommGroup β] : ContinuousAdd (BoundedContinuousFunction α β)