inverse_equiv — Mathlib

English

If e is an equivalence, then the inverse of its forward map equals its symmetric map.

Русский

Если e — эквивалент, тогда обратное к его прямому отображению равно его симметричному отображению.

LaTeX

$$$\text{inverse}(e) = e^{-1} = e.symm$$$

Lean4

/-- By definition, if `f` is invertible then `inverse f = f.symm`. -/
@[simp]
theorem inverse_equiv (e : M ≃L[R] M₂) : inverse (e : M →L[R] M₂) = e.symm := by simp [inverse]

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