English
Elements of the closure of S can be generated from the unit and left-multiplication by elements of S; there is a constructive induction principle for left-mass generation.
Русский
Элементы замыкания S можно получить из единицы и левого умножения на элементы S; существует индукционный принцип слева.
LaTeX
$$closure_induction_left ... p x h$$
Lean4
/-- For subgroups generated by a single element, see the simpler `zpow_induction_left`. -/
@[to_additive (attr := elab_as_elim) /-- For additive subgroups generated by a single element, see the simpler
`zsmul_induction_left`. -/
]
theorem closure_induction_left {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
(mul_left : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x * y) (mul_mem (subset_closure hx) hy))
(inv_mul_cancel : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x⁻¹ * y) (mul_mem (inv_mem (subset_closure hx)) hy))
{x : G} (h : x ∈ closure s) : p x h := by
revert h
simp_rw [← mem_toSubmonoid, closure_toSubmonoid] at *
intro h
induction h using Submonoid.closure_induction_left with
| one => exact one
| mul_left x hx y hy ih =>
cases hx with
| inl hx => exact mul_left _ hx _ hy ih
| inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih
