IsPos

Mathlib.LinearAlgebra.RootSystem.Base

URI: https://scilib.ai/kg/mathlib#RootPairing.Base.IsPos

English

IsPos(i) is the predicate that the corresponding height is positive.

Русский

IsPos(i) — предикат, означающий, что соответствующая высота положительна.

LaTeX

$$IsPos(i) : Prop := 0 < b.height(i)$$

Lean4

/-- The predicate that a (co)root is positive with respect to a base. -/
def IsPos (i : ι) : Prop :=
  0 < b.height i

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

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

Разделы

Аффилиация

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