English
The inverse of the canonical linear equivalence associated to an independent family maps an element x in p_i to the corresponding coordinate vector supported at i.
Русский
Обратное отображение канонического линейного эквивалента для независимого семейства отображает элемент x из p_i в соответствующий вектор-координату, поддерживаемый в i.
LaTeX
$$theorem iSupIndep.linearEquiv_symm_apply (ind) (iSup_top) {i} {x} (h : x ∈ p i) : (ind.linearEquiv iSup_top).symm x = .single i ⟨x, h⟩$$
Lean4
theorem linearEquiv_symm_apply {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤) {i : ι} {x : N}
(h : x ∈ p i) : (ind.linearEquiv iSup_top).symm x = .single i ⟨x, h⟩ := by
simp [← LinearEquiv.eq_symm_apply, iSupIndep.linearEquiv]
