to_isOrderedModule — Mathlib

English

If a cone C defines the order by x ≤ y iff y − x ∈ C, then E becomes an ordered R-module.

Русский

Если конус C задаёт порядок по формуле x ≤ y ⇔ y − x ∈ C, то E образует упорядоченный модуль над R.

LaTeX

$$$(\forall x,y\in E)\ x \le y \iff y-x \in C \quad\Rightarrow\quad IsOrderedModule\,R\,E$$

Lean4

/-- Constructs an ordered module given an ordered group, a cone, and a proof that
the order relation is the one defined by the cone. -/
theorem to_isOrderedModule (C : PointedCone R E) (h : ∀ x y : E, x ≤ y ↔ y - x ∈ C) : IsOrderedModule R E :=
  .of_smul_nonneg <| by simp +contextual [h, C.smul_mem]

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