closure_addSubmonoid_closure — Mathlib

English

closure of the image of AddSubmonoid.closure s equals closure s.

Русский

Замыкание образа AddSubmonoid.closure s равно closure s.

LaTeX

$$closure(↑(AddSubmonoid.closure s)) = closure s$$

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 (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

Похожие утверждения