restrictLatticeHom_apply — Mathlib

English

The lattice-hom restrict map agrees with the pointwise restriction on the elements D.

Русский

Гомоморфизм решётки restrictLatticeHom совпадает с точечным ограничением на элементе D.

LaTeX

$$$\\text{restrictLatticeHom}_h(D) = D.restrict h$$$

Lean4

@[simp]
theorem restrictLatticeHom_apply [AddCommGroup Y] [Lattice Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) :
    restrictLatticeHom h D = D.restrict h := by rfl

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