isStrictlyPositive

Mathlib.Algebra.Algebra.StrictPositivity

URI: https://scilib.ai/kg/mathlib#IsUnit.isStrictlyPositive

← MathLib Explorer

English

If a is a unit and a ≥ 0, then IsStrictlyPositive a.

Русский

Если a единица и a ≥ 0, тогда IsStrictlyPositive a.

LaTeX

$$$ \\mathrm{IsUnit}(a) \\land 0 \\le a \\rightarrow \\mathrm{IsStrictlyPositive}(a) $$$

Lean4

theorem _root_.IsUnit.isStrictlyPositive [LE A] [Monoid A] [Zero A] {a : A} (ha : IsUnit a) (ha₀ : 0 ≤ a) :
    IsStrictlyPositive a :=
  iff_of_unital.mpr ⟨ha₀, ha⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru