pow_mem_pow — Mathlib

English

Let α be a monoid and s ⊆ α with a ∈ s. Then for every natural number n, a^n belongs to s^n, the n-fold product set of elements from s.

Русский

Пусть α — моноид, и s ⊆ α с элементом a ∈ s. Тогда для каждого натурального n выполняется a^n ∈ s^n, где s^n − n-разовая произведение элементов из s.

LaTeX

$$$\forall \alpha\ [Monoid\ \alpha], \forall s \subseteq \alpha, \forall a \in s, \\ \forall n \in \mathbb{N}, a^n \in s^n$$$

Lean4

@[to_additive]
theorem pow_mem_pow (ha : a ∈ s) : a ^ n ∈ s ^ n := by simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

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