English
A version of Pi.continuousInv for non-dependent functions; it asserts ContinuousInv (ι → G) using Pi.continuousInv.
Русский
Версия Pi.continuousInv для не зависимых функций; утверждает ContinuousInv (ι → G) через Pi.continuousInv.
LaTeX
$$$\\\\operatorname{ContinuousInv} (\\\\iota \\to G).$$$
Lean4
/-- A version of `Pi.continuousInv` for non-dependent functions. It is needed because sometimes
Lean fails to use `Pi.continuousInv` for non-dependent functions. -/
@[to_additive /-- A version of `Pi.continuousNeg` for non-dependent functions. It is needed
because sometimes Lean fails to use `Pi.continuousNeg` for non-dependent functions. -/
]
instance has_continuous_inv' : ContinuousInv (ι → G) :=
Pi.continuousInv
