strictMono

Mathlib.Order.JordanHolder

URI: https://scilib.ai/kg/mathlib#CompositionSeries.strictMono

← MathLib Explorer

English

A composition series induces a strictly monotone function.

Русский

Составная серия порождает строго монотонную отображение.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ (s : \\mathrm{CompositionSeries}\\ X)\\ \\to\\mathrm{StrictMono}\\ s.$$$

Lean4

protected theorem strictMono (s : CompositionSeries X) : StrictMono s :=
  Fin.strictMono_iff_lt_succ.2 s.lt_succ

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

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

Разделы

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

Аффилиация

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