continuousInv — Mathlib

English

If f: G → H is inducing and preserves inverses in the sense f(x)⁻¹ = (f(x))⁻¹, then G has continuous inversion.

Русский

Если отображение f: G → H индукцирует топологию на G и сохраняет инверсию в смысле f(x)⁻¹ = f(x⁻¹), то G имеет непрерывную инверсію.

LaTeX

$$$IsInducing(f) \land (\forall x, f(x)^{-1} = (f(x))^{-1}) \Rightarrow \text{ContinuousInv}(G).$$$

Lean4

@[to_additive]
theorem continuousInv {G H : Type*} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H]
    {f : G → H} (hf : IsInducing f) (hf_inv : ∀ x, f x⁻¹ = (f x)⁻¹) : ContinuousInv G :=
  ⟨hf.continuous_iff.2 <| by simpa only [Function.comp_def, hf_inv] using hf.continuous.inv⟩

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