to_continuousDiv — Mathlib

English

If G is a topological group, the division map (x,y) ↦ x y^{-1} is continuous.

Русский

Пусть G — топологическая группа. Операция деления (x,y) ↦ x y^{-1} непрерывна.

LaTeX

$$$\\mathrm{ContinuousDiv}\\, G$$$

Lean4

@[to_additive]
instance (priority := 100) to_continuousDiv {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    ContinuousDiv G where
  continuous_div' := by
    simp only [div_eq_mul_inv]
    exact continuous_mul.comp₂ continuous_fst <| continuous_inv.comp continuous_snd

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