inverse_apply_eq — Mathlib

English

For an invertible f, f.inverse y = x if and only if y = f x.

Русский

Для обратимого $f$ верно: $f^{-1}(y) = x$ тогда и только тогда, когда $y = f(x)$.

LaTeX

$$$\forall x \;\forall y: M_2,\; f^{-1}(y) = x \iff y = f(x)$$$

Lean4

theorem inverse_apply_eq {f : M →L[R] M₂} {x : M} {y : M₂} (hf : f.IsInvertible) : f.inverse y = x ↔ y = f x :=
  by
  rcases hf with ⟨M, rfl⟩
  simp only [inverse_equiv, ContinuousLinearEquiv.coe_coe]
  exact ContinuousLinearEquiv.symm_apply_eq M

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