instContinuousInvMultiplicativeOfContinuousNeg

English

If H has a topological space, a Neg operation, and continuousNeg, then ContinuousInv (Multiplicative H) holds.

Русский

Если у H есть топологическое пространство, операция Neg и continuousNeg, то ContinuousInv (Multiplicative H) выполняется.

LaTeX

$$$\\\\operatorname{ContinuousInv} (\\\\operatorname{Multiplicative} H).$$$

Lean4

instance [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousInv (Multiplicative H) where
  continuous_inv := @continuous_neg H _ _ _

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