English
Every element x of the free commutative ring has finite support: there exists a finite subset s of α such that IsSupported(x, s).
Русский
Каждый элемент x свободного коммутативного кольца имеет конечную опору: существует конечное подмножество s ⊆ α такое, что IsSupported(x, s).
LaTeX
$$$\\exists s : Set\\,\\alpha, \\operatorname{Finite}(s) \\land \\mathrm{IsSupported}(x, s)$$$
Lean4
theorem exists_finite_support (x : FreeCommRing α) : ∃ s : Set α, Set.Finite s ∧ IsSupported x s :=
FreeCommRing.induction_on x ⟨∅, Set.finite_empty, isSupported_neg isSupported_one⟩
(fun p => ⟨{ p }, Set.finite_singleton p, isSupported_of.2 <| Set.mem_singleton _⟩)
(fun _ _ ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩ =>
⟨s ∪ t, hfs.union hft,
isSupported_add (isSupported_upwards hxs Set.subset_union_left)
(isSupported_upwards hxt Set.subset_union_right)⟩)
fun _ _ ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩ =>
⟨s ∪ t, hfs.union hft,
isSupported_mul (isSupported_upwards hxs Set.subset_union_left) (isSupported_upwards hxt Set.subset_union_right)⟩
