restrictSupportEquiv_symm_apply_coe

English

The inverse of restrictSupportEquiv applied to f yields f.extendDomain, i.e., the symm image corresponds to extending the domain.

Русский

ОбратноеRestrictSupportEquiv, применённое к f, даёт f.extendDomain; образ симм соответствует расширению области определения.

LaTeX

$$$(\\mathrm{restrictSupportEquiv}(s,M))^{-1} f = f.\\extendDomain$$$

Lean4

@[simp]
theorem restrictSupportEquiv_symm_apply_coe (s : Set α) (M : Type*) [AddCommMonoid M] [DecidablePred (· ∈ s)]
    (f : s →₀ M) : (restrictSupportEquiv s M).symm f = f.extendDomain := by
  rw [restrictSupportEquiv, Equiv.coe_fn_symm_mk, Subtype.coe_mk]; congr

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