English
An induction principle for closure membership with respect to additive submonoid structure: if a property holds for 0, 1, and is closed under addition and multiplication, then it holds for all elements of closure(s).
Русский
Индукционная принципия для замыкания относительно аддитивного подмоноида: если свойство верно для 0, 1 и сохраняется при сложении и умножении, то верно для всех элементов closure(s).
LaTeX
$$@[elab_as_elim] closure_induction ...$$
Lean4
@[simp]
theorem closure_addSubmonoid_closure {s : Set R} : closure ↑(AddSubmonoid.closure s) = closure s :=
by
ext x
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
rintro - ⟨H, rfl⟩
rintro - ⟨J, rfl⟩
refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_
refine (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => ?_
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw
