instContinuousInv₀ — Mathlib

English

Let Γ₀ be a linearly ordered commutative group with zero, endowed with the zero-adapted topology. Then the inversion operation x ↦ x⁻¹ is continuous at every nonzero element.

Русский

Пусть Γ₀ — линейно упорядоченная коммутативная группа с нулём, на неё задана нулевая топология. Тогда отображение x ↦ x⁻¹ непрерывно в каждой ненулевой точке.

LaTeX

$$$$ \forall \gamma \neq 0,\; \mathrm{ContinuousAt}(\lambda x:\Gamma_0, x^{-1}) (\gamma). $$$$

Lean4

@[nolint defLemma]
scoped instance (priority := 100) : ContinuousInv₀ Γ₀ :=
  ⟨fun γ h => by
    rw [ContinuousAt, nhds_of_ne_zero h]
    exact pure_le_nhds γ⁻¹⟩

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