English
For x ∈ closure(s), there exists a list L of lists of elements of R such that each inner list consists of elements from s or equal to −1, and the sum of products of the inner lists equals x.
Русский
Для x ∈ closure(s) существует список L из списков элементов R, где каждый элемент внутреннего списка принадлежит s или равен −1, и сумма произведений элементов по каждому списку равна x.
LaTeX
$$$\\exists L : \\mathrm{List}(\\mathrm{List}\\,R),\\ (\\forall t \\in L, \\forall y \\in t, y \\in s \\lor y = -1) \\land (\\mathrm{List.map}\\, \\mathrm{List.prod}\\, L).\\mathrm{sum} = x$$$
Lean4
theorem exists_list_of_mem_closure {s : Set R} {x : R} (hx : x ∈ closure s) :
∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = (-1 : R)) ∧ (L.map List.prod).sum = x :=
by
rw [mem_closure_iff] at hx
induction hx using AddSubgroup.closure_induction with
| mem _ hx =>
obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx
exact ⟨[l], by simp [h]; clear_aux_decl; tauto⟩
| zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
| add _ _ _ _ hL hM =>
obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by rw [List.map_append, List.sum_append, HL2, HM2]⟩
| neg _ _ hL =>
obtain ⟨L, hL⟩ := hL
exact
⟨L.map (List.cons (-1)), List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
hL.2 ▸ List.recOn L (by simp) (by simp +contextual [List.map_cons, add_comm])⟩
