pow_mem_pow — Mathlib

English

If s ∈ f, then s^n ∈ f^n for every n ∈ ℕ.

Русский

Если множество s принадлежит фильтру f, то s^n принадлежит f^n для любого n ∈ ℕ.

LaTeX

$$$\forall s \in f,\ \forall n \in \mathbb{N},\ s^n \in f^n.$$$

Lean4

@[to_additive]
theorem pow_mem_pow (hs : s ∈ f) : ∀ n : ℕ, s ^ n ∈ f ^ n
  | 0 => by
    rw [pow_zero]
    exact one_mem_one
  | n + 1 => by
    rw [pow_succ]
    exact mul_mem_mul (pow_mem_pow hs n) hs

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