instContinuousInv — Mathlib

English

If G has Inv and ContinuousInv, then the inversion on SeparationQuotient G is continuous.

Русский

Если у G есть инверсия и непрерывная инверсия, то инверсия на SeparationQuotient(G) непрерывна.

LaTeX

$$$\operatorname{ContinuousInv}(\mathrm{SeparationQuotient}(G))$$$

Lean4

@[to_additive]
instance instContinuousInv [Inv G] [ContinuousInv G] : ContinuousInv (SeparationQuotient G) where
  continuous_inv := isQuotientMap_mk.continuous_iff.2 <| continuous_mk.comp continuous_inv

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