subset_coe_pow — Mathlib

English

The nth NPow of the underlying SubMulAction’s coefficient is contained in the corresponding Set power of the underlying set.

Русский

N-я степень NPow подмножества содержится в соответствующей степени множества.

LaTeX

$$$\\mathrm{subset\\_coe\\_pow}(p) : (p^{n}) \\subseteq (p)^{n}$$$

Lean4

theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, (p : Set M) ^ n ⊆ ↑(p ^ n)
  | 0 => by
    rw [pow_zero, pow_zero]
    exact subset_coe_one
  | n + 1 => by rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]

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