restrictSupportEquiv_symm_single — Mathlib

English

The inverse of restrictSupportEquiv applied to the singleton on a ∈ s with value x is the singleton at a viewed as α-element.

Русский

Обратное RestrictSupportEquiv применимо к единичной функции на a ∈ s с значением x — это единичная функция на a, разглядываемая как элемент α.

LaTeX

$$$(\\mathrm{restrictSupportEquiv}(s,M))^{-1} (\\mathrm{single}\\ a x) = \\mathrm{single}(a:\\alpha) x$$$

Lean4

@[simp]
theorem restrictSupportEquiv_symm_single (s : Set α) (M : Type*) [AddCommMonoid M] (a : s) (x : M) :
    (restrictSupportEquiv s M).symm (single a x) = single (a : α) x := by classical simp

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