English
If s is linear, then closure(s) is semilinear.
Русский
Если s линейно, то closure(s) семилинейно.
LaTeX
$$$IsLinearSet(s) \Rightarrow IsSemilinearSet(closure s).$$$
Lean4
protected theorem closure (hs : IsLinearSet s) : IsSemilinearSet (closure s : Set M) :=
by
rcases hs with ⟨a, t, ht, rfl⟩
convert (IsSemilinearSet.singleton 0).union (isSemilinearSet ⟨a, { a } ∪ t, by simp [ht], rfl⟩)
ext x
simp only [SetLike.mem_coe, singleton_union, mem_insert_iff, mem_vadd_set, vadd_eq_add]
constructor
· intro hx
induction hx using closure_induction with
| mem x hx =>
rcases hx with ⟨x, hx, rfl⟩
exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩
| zero => exact Or.inl rfl
| add x y _ _ ih₁ ih₂ =>
rcases ih₁ with rfl | ⟨x, hx, rfl⟩
· simpa
· rcases ih₂ with rfl | ⟨y, hy, rfl⟩
· exact Or.inr ⟨x, hx, by simp⟩
· refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
simp_rw [← add_assoc, add_right_comm a a x]
· rintro (rfl | ⟨x, hx, rfl⟩)
· simp
· simp_rw [insert_eq, closure_union, mem_sup, mem_closure_singleton] at hx
rcases hx with ⟨_, ⟨n, rfl⟩, ⟨x, hx, rfl⟩⟩
rw [add_left_comm]
refine add_mem (nsmul_mem (mem_closure_of_mem ?_) _) (mem_closure_of_mem (vadd_mem_vadd_set hx))
nth_rw 2 [← add_zero a]
exact vadd_mem_vadd_set (zero_mem _)
