ContinuousMul in a LinearOrderedSemifield?

Stream: maths

[Yury G. Kudryashov]

I'm trying to generalize some limits from [LinearOrderedField k] to [LinearOrderedSemifield k]. What are the right assumptions to get:

• ContinuousAdd?
• ContinuousMul?
• Tendsto f l atTop → Tendsto (fun x => C / f x) l (nhds 0)?

[Yury G. Kudryashov]

Or should I just assume [ContinuousMul k] / [ContinuousAdd k] whenever it's convenient, since all linearly ordered semifields we use (incl. all linearly ordered fields and Nonneg _) have these properties anyway?

[Yaël Dillies]

I would just assume ContinuousMul k/ContinuousAdd k where convenient

[Yury G. Kudryashov]

OK, #23859 (depends on #23857)