salient_positive — Mathlib

English

The positive cone of an ordered module is salient; i.e., it contains no nonzero element together with its negation.

Русский

Положительный конус упорядоченного модуля является salient; то есть в нём не содержится ненулевой элемент вместе с его отрицанием.

LaTeX

$$Salient(positive(R,M))$$

Lean4

/-- The positive cone of an ordered module is always salient. -/
theorem salient_positive {G : Type*} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module R G]
    [PosSMulMono R G] : Salient (positive R G) := fun x hx_nonneg hx_ne_zero hx_nonpos ↦
  lt_irrefl (0 : G) <| by simpa using add_pos_of_nonneg_of_pos hx_nonpos <| hx_nonneg.lt_of_ne' hx_ne_zero

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