English
If M is a monoid acting by multiplication on F and certain compatibility holds, UniformConvergenceCLM σ F 𝔖 becomes a distributive-multiplicative action space over M.
Русский
Если M действует на F умножением и соблюдены условия совместимости, то UniformConvergenceCLM σ F 𝔖 образует пространство с действием распределимого умножения над M.
LaTeX
$$$\\text{DistribMulAction } M (\\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S}))$$$
Lean4
theorem t2Space [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) :
T2Space (UniformConvergenceCLM σ F 𝔖) :=
by
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
exact (isEmbedding_coeFn σ F 𝔖).t2Space
