mk_pow — Mathlib

English

Exponentiation on the nonnegative subtype is given by lifting the ambient power to the subtype.

Русский

Возведение в степень на подтипе неотрицательных элементов задаётся подниманием степени в окружение к подтипу.

LaTeX

$$$ (\langle x, hx \rangle)^n = \langle x^n, pow\_nonneg hx n \rangle $$$

Lean4

@[simp]
theorem mk_pow {x : α} (hx : 0 ≤ x) (n : ℕ) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, pow_nonneg hx n⟩ :=
  rfl

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