sup_pow_add_le_pow_sup_pow — Mathlib

English

For two ideals I and J and natural numbers n,m, we have (I ⊔ J)^{n+m} ≤ I^n ⊔ J^m.

Русский

Для двух идеалов I и J и натуральных чисел n,m выполняется (I ⊔ J)^{n+m} ≤ I^n ⊔ J^m.

LaTeX

$$$ (I \\sqcup J)^{n+m} \\le I^{n} \\sqcup J^{m} $$$

Lean4

theorem sup_pow_add_le_pow_sup_pow {n m : ℕ} : (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m :=
  by
  rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup]
  apply Finset.sup_le
  intro i hi
  by_cases hn : n ≤ i
  · exact (Ideal.mul_le_right.trans (Ideal.mul_le_right.trans ((Ideal.pow_le_pow_right hn).trans le_sup_left)))
  · refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))
    cutsat

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