restrictMonoidHom — Mathlib

English

Restriction defines a monoid hom from functions on U to functions on V by restricting their domain.

Русский

Ограничение задаёт однородный по операции сложения гомоморфизм от функций на U к функциям на V за счёт ограничения области определения.

LaTeX

$$$\\text{restrictMonoidHom}(h) : \\text{LocallyFinsuppWithin}(U,Y) \\to+\\text{LocallyFinsuppWithin}(V,Y)$ with $toFun(D) = D.restrict h$$$

Lean4

/-- Restriction as a group morphism -/
noncomputable def restrictMonoidHom [AddCommGroup Y] {V : Set X} (h : V ⊆ U) :
    locallyFinsuppWithin U Y →+ locallyFinsuppWithin V Y
    where
  toFun D := D.restrict h
  map_zero' := by
    ext x
    simp [restrict_apply]
  map_add' D₁
    D₂ := by
    ext x
    by_cases hx : x ∈ V <;> simp [restrict_apply, hx]

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