inv_spec — Mathlib

English

The inverse in the monoid of generalized loops corresponds to the generalized loop symmetry along a fixed coordinate.

Русский

Обратное в моноиде обобщённых петель соответствует симметрии обобщённой петли по фиксированной координате.

LaTeX

$$$\\mathrm{inv}([p]) = [\\mathrm{symmAt}\\ i\\ p]$$$

Lean4

/-- Characterization of multiplicative inverse -/
theorem inv_spec [Nonempty N] {i} {p : Ω^ N X x} : ((⟦p⟧)⁻¹ : HomotopyGroup N X x) = ⟦symmAt i p⟧ :=
  by
  rw [symmAt_indep (Classical.arbitrary N) p, ← fromLoop_symm_toLoop]
  apply Quotient.sound
  rfl

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