supportedEquivFinsupp_symm_apply_coe

English

A related comap inequality for restricted domains holds

Русский

Справедливо неравенство для обратного отображения при ограничении области определения.

LaTeX

$$$\mathrm{supported}(M,R, f^{-1}'s) \le \mathrm{comap}(\mathrm{lmapDomain}(M,R,f), \mathrm{supported}(M,R, s))$$$

Lean4

@[simp]
theorem supportedEquivFinsupp_symm_apply_coe (s : Set α) [DecidablePred (· ∈ s)] (f : s →₀ M) :
    (supportedEquivFinsupp (R := R) s).symm f = f.extendDomain := by convert restrictSupportEquiv_symm_apply_coe ..

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