English
If M is a commutative monoid with a suitable topology, and the same nhds-at-1 convergence and left/right conditions hold, then ContinuousMul M.
Русский
Если M коммутативный моноид с подходящей топологией, и выполняются условия стержневок по nhds при единице, тогда ContinuousMul M.
LaTeX
$$$[CommMonoid\\,M] \\land [TopologicalSpace\\,M] \\land \\ Tendsto(\\text{uncurry}((\\cdot * \\cdot)))(\\mathcal{N}(1) \\times \\mathcal{N}(1))(\\mathcal{N}(1)) \\Rightarrow \\text{ContinuousMul}\\,M$; additionally, $\\forall x_0,\\ 1$ commutes with translations.$$
Lean4
@[to_additive]
theorem continuousMul_of_comm_of_nhds_one (M : Type u) [CommMonoid M] [TopologicalSpace M]
(hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
(hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)) : ContinuousMul M :=
by
apply ContinuousMul.of_nhds_one hmul hleft
intro x₀
simp_rw [mul_comm, hleft x₀]
