closure_pow — Mathlib

English

For AddSubmonoid s and natural n, s^n equals the closure of the nth power of s viewed as a set: s^n = closure((s : Set R)^n).

Русский

Для аддитивного подпмножества s и натурального n выполняется s^n = closure((s : Set R)^n).

LaTeX

$$$ s^n = \operatorname{closure}((s : Set R)^n) $$$

Lean4

theorem closure_pow (s : Set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_closure_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

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