English
The collection of functions with locally finite support within U forms an additive subgroup of all functions X → Y.
Русский
Собрание функций с локально конечной опорой внутри U образует начертание подгруппы по сложению внутри всех функций X → Y.
LaTeX
$$$\\{ f: X \\to Y : f\\operatorname{supp} \\subseteq U \\;\\wedge\\; \\forall z \\in U, \\exists t \\in \\mathcal{N}(z), |t \\cap \\operatorname{supp}(f)|<\\infty\\}$ является подгруппой сложения в $(X\\to Y)$$$
Lean4
/-- Functions with locally finite support within `U` form an additive subgroup of functions X → Y.
-/
protected def addSubgroup [AddCommGroup Y] : AddSubgroup (X → Y)
where
carrier := {f | f.support ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)}
zero_mem' :=
by
simp only [support_subset_iff, ne_eq, mem_setOf_eq, Pi.zero_apply, not_true_eq_false, IsEmpty.forall_iff,
implies_true, support_zero, inter_empty, finite_empty, and_true, true_and]
exact fun _ _ ↦ ⟨⊤, univ_mem⟩
add_mem' {f g} hf
hg := by
constructor
· intro x hx
contrapose! hx
simp [notMem_support.1 fun a ↦ hx (hf.1 a), notMem_support.1 fun a ↦ hx (hg.1 a)]
· intro z hz
obtain ⟨t₁, ht₁⟩ := hf.2 z hz
obtain ⟨t₂, ht₂⟩ := hg.2 z hz
use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
apply Set.Finite.subset (s := (t₁ ∩ f.support) ∪ (t₂ ∩ g.support)) (ht₁.2.union ht₂.2)
intro a ha
simp_all only [support_subset_iff, ne_eq, mem_setOf_eq, mem_inter_iff, mem_support, Pi.add_apply, mem_union,
true_and]
by_contra hCon
push_neg at hCon
simp_all
neg_mem' {f} hf := by simp_all
