continuous_inv_iff — Mathlib

English

Let G be a topological group with continuous inversion. For any space α and any function f: α → G, the inverse function f⁻¹ is continuous if and only if f is continuous.

Русский

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

LaTeX

$$$\forall G, \alpha, (\text{TopologicalSpace } G) \land (\text{ContinuousInv } G) \land (f: \alpha \to G) \, \Rightarrow \, (\text{Continuous}(f^{-1}) \iff \text{Continuous}(f)).$$$

Lean4

@[to_additive (attr := simp)]
theorem continuous_inv_iff : Continuous f⁻¹ ↔ Continuous f :=
  (Homeomorph.inv G).comp_continuous_iff

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