closure_pow_le — Mathlib

English

If 1 ∈ S and n ≠ 0, then closure(S^n) = closure(S).

Русский

Если 1 ∈ S и n ≠ 0, то closure(S^n) = closure(S).

LaTeX

$$$ closure(S^n) = closure S $ under the given conditions$$

Lean4

@[to_additive]
theorem closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
  | 1, _ => by simp
  | n + 2, _ =>
    calc
      closure (s ^ (n + 2))
      _ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
      _ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
      _ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
      _ = closure s := sup_idem _

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