inv — Mathlib

English

A cycle property is preserved under taking inverses: f is a cycle iff f^{-1} is a cycle.

Русский

Свойство цикла сохраняется при взятии обратной перестановки: f циклическая тогда и только тогда, когда f^{-1} циклична.

LaTeX

$$IsCycle(f^{-1}) ⇔ IsCycle(f)$$

Lean4

theorem inv (hf : IsCycle f) : IsCycle f⁻¹ :=
  hf.imp fun _ ⟨hx, h⟩ => ⟨inv_eq_iff_eq.not.2 hx.symm, fun _ hy => (h <| inv_eq_iff_eq.not.2 hy.symm).inv⟩

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