English
A listed collection of locally constant maps to form a basis for the finite-support product; the list is constructed by taking certain combinations of basic e maps.
Русский
Задаётся список локально константных отображений, образующий базис для произведения с конечной опорой; список строится из комбинаций базовых e отображений.
LaTeX
$$$\\text{factors }(x) : List\\; (LocallyConstant(π C (· ∈ s) .Elem \\mathbb{Z}))$; дальнейшие свойства описаны в theorem.$$
Lean4
theorem span : ⊤ ≤ Submodule.span ℤ (Set.range (spanFinBasis C s)) :=
by
intro f _
rw [Finsupp.mem_span_range_iff_exists_finsupp]
use Finsupp.onFinset (Finset.univ) f.toFun (fun _ _ ↦ Finset.mem_univ _)
ext x
change LocallyConstant.evalₗ ℤ x _ = _
simp only [zsmul_eq_mul, map_finsuppSum, LocallyConstant.evalₗ_apply, LocallyConstant.coe_mul, Pi.mul_apply,
spanFinBasis, LocallyConstant.coe_mk, mul_ite, mul_one, mul_zero, Finsupp.sum_ite_eq, Finsupp.mem_support_iff,
ne_eq, ite_not]
split_ifs with h <;> [exact h.symm; rfl]
