instOneSubtypeLtOfNat_mathlib — Mathlib

English

Let R be a strict ordered ring. Then the positive subtype { x ∈ R | 0 < x } has a multiplicative identity 1, which lies in the positive set.

Русский

Пусть R — строго упорядоченное кольцо. Тогда у положительного подтипа { x ∈ R | 0 < x } есть единица 1, принадлежащая этому множеству.

LaTeX

$$$1 > 0$ and the multiplicative identity in the ambient ring lies in the positive subtype, i.e., 1 \\in { x : R \\mid 0 < x }.$$$

Lean4

instance : One { x : R // 0 < x } :=
  ⟨⟨1, one_pos⟩⟩

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