symm — Mathlib

English

The inverse of an equidecomposition is itself an equidecomposition.

Русский

Обратная эквидекомпозиция остаётся эквидекомпозициями.

LaTeX

$$$\\forall f:\\mathrm{Equidecomp}(X,G),\\; f^{\\mathrm{symm}}\\in \\mathrm{Equidecomp}(X,G).$$$

Lean4

/-- The inverse function of an equidecomposition as an equidecomposition. -/
@[symm, simps toPartialEquiv]
noncomputable def symm (f : Equidecomp X G) : Equidecomp X G
    where
  toPartialEquiv := f.toPartialEquiv.symm
  isDecompOn' := by
    classical
      exact
      ⟨f.witness⁻¹, by
        convert f.isDecompOn.of_leftInvOn f.leftInvOn
        rw [image_source_eq_target, symm_source]⟩

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