English
Restriction acts as a lattice morphism between LocallyFinsuppWithin(U,Y) and LocallyFinsuppWithin(V,Y), preserving both sup and inf.
Русский
Ограничение действует как морфизм решётки между LocallyFinsuppWithin(U,Y) и LocallyFinsuppWithin(V,Y), сохраняя sup и inf.
LaTeX
$$$\\text{restrictLatticeHom}(h) : \\text{LatticeHom}(\\text{LocallyFinsuppWithin}(U,Y), \\text{LocallyFinsuppWithin}(V,Y))$ with $\\text{map\_sup'}$ and $\\text{map\_inf'}$ defined by pointwise restriction$$
Lean4
/-- Restriction as a lattice morphism -/
noncomputable def restrictLatticeHom [AddCommGroup Y] [Lattice Y] {V : Set X} (h : V ⊆ U) :
LatticeHom (locallyFinsuppWithin U Y) (locallyFinsuppWithin V Y)
where
toFun D := D.restrict h
map_sup' D₁
D₂ := by
ext x
by_cases hx : x ∈ V <;> simp [locallyFinsuppWithin.restrict_apply, hx]
map_inf' D₁
D₂ := by
ext x
by_cases hx : x ∈ V <;> simp [locallyFinsuppWithin.restrict_apply, hx]
