pow_subset_pow

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.pow_subset_pow

English

For AddSubmonoid s and natural n, the nth power of the underlying set is contained in the underlying set of s^n: (↑s : Set R)^n ⊆ ↑(s^n).

Русский

Для AddSubmonoid s и натурального n: (↑s : Set R)^n ⊆ ↑(s^n).

LaTeX

$${(s : Set R)}^n \subseteq (s^n : Set R)$$

Lean4

theorem pow_subset_pow {s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ ↑(s ^ n) :=
  (pow_eq_closure_pow_set s n).symm ▸ subset_closure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru