IsStrictlyPositive — Mathlib

English

IsStrictlyPositive a is defined as a is nonnegative and a is a unit.

Русский

IsStrictlyPositive a задается как a является неотрицательным и единицей (обращаемым).

LaTeX

$$$ \\mathrm{IsStrictlyPositive}(a) \\;\\text{is by definition } 0 \\le a \\wedge \\mathrm{IsUnit}(a). $$$

Lean4

/-- An element of an ordered algebra is *strictly positive* if it is nonnegative and invertible.

NOTE: This definition will be generalized to the non-unital case in the future; do not unfold
the definition and use the API provided instead to avoid breakage when the refactor happens. -/
def IsStrictlyPositive {A : Type*} [LE A] [Monoid A] [Zero A] (a : A) : Prop :=
  0 ≤ a ∧ IsUnit a

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