English
If a monoid M has a neighborhood structure at 1 that is compatible with multiplication in the way described (a_hmul tends to 1 from 𝓝1 × 𝓝1, with left and right translations of 1 aligning with 𝓝1), then multiplication on M is continuous.
Русский
Если для моноида M соседей в точке 1 достаточно, чтобы выполнялись условия: умножение стремится к 1 при приближении к (1,1), слева и справа переносы по 1 согласованы с 𝓝1, то умножение непрерывно.
LaTeX
$$$\\text{hmul}:\\ Tendsto(\\text{uncurry}((\\cdot * \\cdot)))(\\mathcal{N}(1) \\times \\mathcal{N}(1)) \\to \\mathcal{N}(1)$, $\\forall x_0: M,\\ \\mathcal{N}(x_0)=\\text{map}(\\lambda x, x_0 x)(\\mathcal{N}(1))$, $\\forall x_0: M,\\ \\mathcal{N}(x_0)=\\text{map}(\\lambda x, x x_0)(\\mathcal{N}(1)) \\Rightarrow \\text{ContinuousMul}\\,M$$$
Lean4
@[to_additive]
theorem of_nhds_one {M : Type u} [Monoid M] [TopologicalSpace M]
(hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) <| 𝓝 1)
(hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)) (hright : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) :
ContinuousMul M :=
⟨by
rw [continuous_iff_continuousAt]
rintro ⟨x₀, y₀⟩
have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) :=
by
ext p
simp [uncurry, mul_assoc]
have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x :=
by
ext x
simp [mul_assoc]
calc
map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by rw [nhds_prod_eq]
_ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) :=
by
unfold uncurry
rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
_ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by
rw [key, ← Filter.map_map]
_ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := (map_mono hmul)
_ = 𝓝 (x₀ * y₀) := by rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]⟩
