English
If Y has a semilattice infimum and zero, LocallyFinsuppWithin carries a Min structure defined pointwise by (D1 ∧ D2)(x) = min(D1(x), D2(x)).
Русский
Если у Y есть Infimum, LocallyFinsuppWithin имеет структуру Min, где (D1 ∧ D2)(x) = min(D1(x), D2(x)).
LaTeX
$$$\\min(D_1, D_2) \\;:\\; X \\to Y\\quad (\\min(D_1, D_2))(x) = \\min(D_1(x), D_2(x))$$$
Lean4
instance [SemilatticeInf Y] [Zero Y] : Min (locallyFinsuppWithin U Y) where
min D₁
D₂ :=
{ toFun z := min (D₁ z) (D₂ z)
supportWithinDomain' := by
intro x
contrapose
intro hx
simp [notMem_support.1 fun a ↦ hx (D₁.supportWithinDomain a),
notMem_support.1 fun a ↦ hx (D₂.supportWithinDomain a)]
supportLocallyFiniteWithinDomain' := by
intro z hz
obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
intro a ha
simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
by_contra hCon
push_neg at hCon
simp_all }
