basis_natDegree_strictMono

Mathlib.Algebra.Polynomial.Sequence

URI: https://scilib.ai/kg/mathlib#Polynomial.Sequence.basis_natDegree_strictMono

← MathLib Explorer

English

NatDegree of basis elements is strictly increasing with the index.

Русский

NatDegree элементов базиса строго возрастает с индексом.

LaTeX

$$StrictMono (natDegree ∘ (S.basis hCoeff)).$$

Lean4

/-- Basis elements have strictly monotone natural degree. -/
theorem basis_natDegree_strictMono : StrictMono <| natDegree ∘ (S.basis hCoeff) := fun _ _ ↦ by simp

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

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

Разделы

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

Аффилиация

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