English
x ∈ closure s if and only if x ∈ AddSubgroup.closure (Subsemigroup.closure s).
Русский
x ∈ closure s тогда и только тогда, когда x ∈ AddSubgroup.closure (Subsemigroup.closure s).
LaTeX
$$$x \\in \\mathrm{closure}(s) \\iff x \\in \\mathrm{AddSubgroup}.closure(\\mathrm{Subsemigroup}.closure(s))$$$
Lean4
theorem mem_closure_iff {s : Set R} {x} : x ∈ closure s ↔ x ∈ AddSubgroup.closure (Subsemigroup.closure s : Set R) :=
⟨fun h => by
induction h using closure_induction with
| mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
| zero => exact zero_mem _
| add _ _ _ _ hx hy => exact add_mem hx hy
| neg x _ hx => exact neg_mem hx
| mul _ _ _hx _hy hx hy =>
clear _hx _hy
induction hx, hy using AddSubgroup.closure_induction₂ with
| mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
| zero_left => simp
| zero_right => simp
| add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
| add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
| neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
| neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h,
fun h => by
induction h using AddSubgroup.closure_induction with
| mem _ hx =>
induction hx using Subsemigroup.closure_induction with
| mem _ h => exact subset_closure h
| mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
| zero => exact zero_mem _
| add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
| neg _ _ h => exact neg_mem h⟩
