English
There is a ContinuousInv0 structure on the normed division ring α.
Русский
Для нормированного кольца деления существует структура ContinuousInv0.
LaTeX
$$$\text{ContinuousInv}_0(\alpha)$$$
Lean4
instance (priority := 100) to_continuousInv₀ : ContinuousInv₀ α :=
by
refine ⟨fun r r0 => tendsto_iff_norm_sub_tendsto_zero.2 ?_⟩
have r0' : 0 < ‖r‖ := norm_pos_iff.2 r0
rcases exists_between r0' with ⟨ε, ε0, εr⟩
have : ∀ᶠ e in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε :=
by
filter_upwards [(isOpen_lt continuous_const continuous_norm).eventually_mem εr] with e he
have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
calc
‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ := by
rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, mul_sub, sub_mul, mul_assoc _ e, inv_mul_cancel₀ r0,
mul_inv_cancel₀ e0, one_mul, mul_one]
_ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp
_ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
refine squeeze_zero' (Eventually.of_forall fun _ => norm_nonneg _) this ?_
refine (((continuous_const.sub continuous_id).norm.div_const _).div_const _).tendsto' _ _ ?_
simp
