toList_nodup

Mathlib.Order.JordanHolder

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

← MathLib Explorer

English

The toList of a CompositionSeries has no duplicates.

Русский

Список элементов композиционной серии без повторов.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ (s : \\mathrm{CompositionSeries}\\ X), (RelSeries.toList s).\\mathrm{Nodup}.$$$

Lean4

theorem toList_nodup (s : CompositionSeries X) : s.toList.Nodup :=
  s.toList_sorted.nodup

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

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

Разделы

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

Аффилиация

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