inverse_apply — Mathlib

English

The inverse_apply lemma states that applying the inverse to the forward image yields the quotient class of y.

Русский

Лемма inverse_apply утверждает, что обращение к обратному отображению после прямого даёт класс y в квотиции.

LaTeX

$$inverse_apply (y) : (rTensor.inverse Q hfg hg) ((rTensor Q g) y) = Submodule.Quotient.mk (p := LinearMap.range (rTensor Q f)) y$$

Lean4

theorem inverse_apply (y : N ⊗[R] Q) :
    (rTensor.inverse Q hfg hg) ((rTensor Q g) y) = Submodule.Quotient.mk (p := LinearMap.range (rTensor Q f)) y := by
  rw [rTensor.inverse, rTensor.inverse_of_rightInverse_apply]

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