continuousNeg_of_mul — Mathlib

English

If each R_i is a group and each S_i is a subgroup with compatible topology, then the restricted product is a topological group.

Русский

Если каждый R_i — группа, и каждое S_i — подгруппа совместимой топологии, то ограниченное произведение является топологической группой.

LaTeX

$$$\\mathrm{IsTopologicalGroup}\\left(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{S_i\\}; \\mathrm{cofinite})\\right)$$$

Lean4

/-- If `R` is a ring with a continuous multiplication, then negation is continuous as well since it
is just multiplication with `-1`. -/
theorem continuousNeg_of_mul [TopologicalSpace R] [NonAssocRing R] [ContinuousMul R] : ContinuousNeg R where
  continuous_neg := by simpa using (continuous_const.mul continuous_id : Continuous fun x : R => -1 * x)

Похожие утверждения