inv — Mathlib

English

Pointwise inversion of paths in a topological group: (γ)(t)^{-1} = γ(t)^{-1}.

Русский

Построчная инверсия путей в топологической группе: (γ)(t)^{-1} = γ(t)^{-1}.

LaTeX

$$$(\gamma)^{-1}(t) = (\gamma(t))^{-1}.$$$

Lean4

/-- Pointwise inversion of paths in a topological group. -/
@[to_additive (attr := simps!) /-- Pointwise negation of paths in a topological group. -/
    ]
def inv {a b : X} [Inv X] [ContinuousInv X] (γ : Path a b) : Path a⁻¹ b⁻¹ :=
  γ.map continuous_inv

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