isPos_of_mem_support

Mathlib.LinearAlgebra.RootSystem.Base

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

English

If i is in the support of the base, then i is positive.

Русский

Если i принадлежит поддержке основы, то i положителен.

LaTeX

$$∀ {i}, i ∈ b.support → b.IsPos i$$

Lean4

theorem isPos_of_mem_support {i : ι} (h : i ∈ b.support) : b.IsPos i :=
  by
  rw [isPos_iff, height_one_of_mem_support h]
  exact Int.one_pos

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

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

Разделы

Аффилиация

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