Weaker statement than ContinuousSMul

Stream: Is there code for X?

[Emilie (Shad Amethyst)]

I'm working a proof of Rubin's theorem (which states that there exists a MulActionHom α →[G] β if G acts on α and β in sufficiently nice ways), and the paper I'm following defines a couple of structures, one of them "continuous group action", states that ∀ g : G, Continuous (fun x : α => g • x).

I can see that ContinuousSMul exists, but this is a stronger statement than what I need, as it would require that G is a topology. Is there something akin to what I need in mathlib, that doesn't require that G is a topology?

For reference, my current WIP proof resides at https://github.com/adri326/rubin-lean4/
I'm also planning on contributing that proof to mathlib, once I finished proving it in Lean and cleaned it up enough for it to be ready for becoming part of a PR.

[Eric Wieser]

docs#ContinuousConstSMul

[Junyan Xu]

I like the emojis in your commit messages :) However, the repo readme talks about two groups acting on one space, which seems to be in disagreement from the arxiv abstract and what you write above ...

[Emilie (Shad Amethyst)]

Whoops, you're right, it should be one group acting on two spaces