pow_subset_pow_mul_of_sq_subset_mul

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.pow_subset_pow_mul_of_sq_subset_mul

← MathLib Explorer

English

If s^2 ⊆ t s and n ≠ 0, then s^n ⊆ t^{n-1} s.

Русский

Если s^2 ⊆ t s и n ≠ 0, тогда s^n ⊆ t^{n-1} s.

LaTeX

$$$s^2 \\subseteq t s \\;\\Rightarrow\\; n \\neq 0 \\Rightarrow s^n \\subseteq t^{n-1} \\cdot s$$$

Lean4

@[to_additive]
theorem pow_subset_pow_mul_of_sq_subset_mul (hst : s ^ 2 ⊆ t * s) (hn : n ≠ 0) : s ^ n ⊆ t ^ (n - 1) * s :=
  subset_of_le (pow_le_pow_mul_of_sq_le_mul hst hn)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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