continuousAt_inv_iff — Mathlib

English

Let G be a topological group with continuous inversion. For every α, every f: α → G and every x ∈ α, the continuity of f⁻¹ at x is equivalent to the continuity of f at x.

Русский

Пусть G — топологическая группа с непрерывной операцией инверсии. Для всякой f: α → G и каждого x ∈ α непрерывность f⁻¹ в x эквивалентна непрерывности f в x.

LaTeX

$$$\forall f:\alpha \to G, \forall x:\alpha, \text{ContinuousAt}(f^{-1},x) \iff \text{ContinuousAt}(f,x).$$$

Lean4

@[to_additive (attr := simp)]
theorem continuousAt_inv_iff : ContinuousAt f⁻¹ x ↔ ContinuousAt f x :=
  (Homeomorph.inv G).comp_continuousAt_iff _ _

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