strictlyPositive — Mathlib

English

Membership in the strictly positive cone is equivalent to strict positivity: x ∈ strictlyPositive(R,M) ⇔ 0 < x.

Русский

Членство в строго положительном конусе эквивалентно строгой положительности: x ∈ strictlyPositive(R,M) ⇔ 0 < x.

LaTeX

$$x \\in strictlyPositive(R,M) \\iff 0 < x$$

Lean4

/-- The cone of strictly positive elements.

Note that this naming diverges from the mathlib convention of `pos` and `nonneg` due to "positive
cone" (`ConvexCone.positive`) being established terminology for the non-negative elements. -/
def strictlyPositive : ConvexCone R M where
  carrier := Set.Ioi 0
  smul_mem' _ hc _ (hx : _ < _) := smul_pos hc hx
  add_mem' _ hx _ hy := add_pos hx hy

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