inv — Mathlib

English

In a topological group with inversion, the inverse image of a path-connected set is path-connected.

Русский

В топологической группе с инверсией образ обратной карты от связного по траекториям множества сохраняет связь по траекториям.

LaTeX

$$$$\text{If } G\text{ has inv and is path-connected, then } s^{-1} \text{ is path-connected whenever } s \text{ is.}$$$$

Lean4

@[to_additive]
theorem inv {G : Type*} [InvolutiveInv G] [TopologicalSpace G] [ContinuousInv G] {s : Set G} (hs : IsPathConnected s) :
    IsPathConnected s⁻¹ :=
  let ⟨a, ha_mem, ha⟩ := hs
  ⟨a⁻¹, inv_mem_inv.mpr ha_mem, fun x hx ↦ by simpa using ha (mem_inv.mp hx) |>.map continuous_inv⟩

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