pos — Mathlib

English

The set of elements strictly greater than zero forms a submonoid of the ambient monoid α.

Русский

Множество элементов, больших нуля, образует подмоной α.

LaTeX

$$$$ \operatorname{pos}(\alpha) = \{ a \in \alpha \mid 0 < a \}, \quad 1 \in \operatorname{pos}(\alpha), \quad \forall a,b \in \operatorname{pos}(\alpha), ab \in \operatorname{pos}(\alpha). $$$$

Lean4

/-- The submonoid of positive elements. -/
@[simps]
def pos : Submonoid α where
  carrier := Set.Ioi 0
  one_mem' := zero_lt_one
  mul_mem' := mul_pos

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