ofBijective_coeLinearMap_of_mem — Mathlib

English

If x belongs to A_i, then applying the canonical linear map to the i-th coordinate recovers x.

Русский

Если x ∈ A_i, то применение канонического линейного отображения к i-ой координате восстанавливает x.

LaTeX

$$$\mathrm{coeLinearMap}(A)(\mathrm{of}\ i\; x) = x.$$$

Lean4

theorem ofBijective_coeLinearMap_of_mem (h : IsInternal A) {i : ι} {x : M} (hx : x ∈ A i) :
    (LinearEquiv.ofBijective (coeLinearMap A) h).symm x i = ⟨x, hx⟩ :=
  h.ofBijective_coeLinearMap_same ⟨x, hx⟩

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