English
If inversion is continuous at the identity and multiplication is continuous, then inversion is continuous at every unit.
Русский
Если обращение непрерывно в тождестве и умножение непрерывно, то обращение непрерывно на каждом элементе с обратимым элементом.
LaTeX
$$$(\\text{Tendsto inv}_{\\mathcal{N}(1)}^{\\mathcal{N}(1)}) \\Rightarrow (\\text{ContinuousInv}_0\\; G_0)$$$
Lean4
/-- If a group with zero has continuous multiplication and `fun x ↦ x⁻¹` is continuous at one,
then it is continuous at any unit. -/
theorem of_nhds_one (h : Tendsto Inv.inv (𝓝 (1 : G₀)) (𝓝 1)) : ContinuousInv₀ G₀ where
continuousAt_inv₀ x
hx := by
have hx' := inv_ne_zero hx
rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx', tendsto_map'_iff, tendsto_comap_iff]
simpa only [Function.comp_def, mul_inv_rev, mul_inv_cancel_right₀ hx']
