inv — Mathlib

English

If there is a path in a topological group G from x to y, then there is a path from x⁻¹ to y⁻¹ in the inverse set, obtained by taking inverses along the path.

Русский

Если существует путь в группе G от x к y, то существует путь от x⁻¹ к y⁻¹ в множестве обратимых элементов, получаемый взятием обратной по пути.

LaTeX

$$JoinedIn s a b → JoinedIn s⁻¹ a⁻¹ b⁻¹$$

Lean4

@[to_additive]
theorem inv {G : Type*} [InvolutiveInv G] [TopologicalSpace G] [ContinuousInv G] {s : Set G} {a b : G}
    (hs : JoinedIn s a b) : JoinedIn s⁻¹ a⁻¹ b⁻¹ :=
  ⟨hs.somePath.inv, fun t ↦ Set.inv_mem_inv.mpr (hs.somePath_mem t)⟩

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