instPowSubtypeLtOfNatNat_mathlib — Mathlib

English

Let R be a strict ordered ring. Then the positive subtype { x ∈ R | 0 < x } is closed under taking natural powers: for x > 0 and n ∈ N, x^n > 0.

Русский

Пусть R — строго упорядченное кольцо. Тогда множество положительных элементов замкнуто относительно возведения в натуральную степень: для x>0 и n ∈ N имеет место x^n > 0.

LaTeX

$$$\\\\forall x \\\\in \\\\{ x : R \\\\mid 0 < x \\\\},\\\\forall n \\\\in \\\\mathbb{N}, \\\\ 0 < x^n.$$$

Lean4

instance : Pow { x : R // 0 < x } ℕ :=
  ⟨fun x n => ⟨(x : R) ^ n, pow_pos x.2 n⟩⟩

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