pow_subset_pow_mul_of_sq_subset_mul

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.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 \;\text{and}\; n \neq 0 \Rightarrow s^n \subseteq t^{n-1} * 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 :=
  pow_le_pow_mul_of_sq_le_mul hst hn

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

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

Разделы

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

Аффилиация

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