closure_pow — Mathlib

English

For any s ⊆ G and n ∈ N with n ≠ 0, closure(s^n) ≤ closure(s).

Русский

Для любого множества s ⊆ G и n ∈ N, n ≠ 0, верно closure(s^n) ⊆ closure(s).

LaTeX

$$$\\forall {n:\\mathbb{N}},\\ n\\neq 0\\Rightarrow \\mathrm{closure}(s^n) \\leq \\mathrm{closure}(s).$$$

Lean4

@[to_additive]
theorem closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn

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