instUnique

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#Flag.instUnique

← MathLib Explorer

English

Over a linear order, there is a unique flag on α.

Русский

Для линейного порядка существует уникальный флаг над α.

LaTeX

$$$[LinearOrder α] \\\\rightarrow Unique (Flag α)$$$

Lean4

instance [LinearOrder α] : Unique (Flag α)
    where
  default := ⟨univ, isChain_of_trichotomous _, fun s _ => s.subset_univ.antisymm'⟩
  uniq s := SetLike.coe_injective <| s.3 (isChain_of_trichotomous _) <| subset_univ _

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

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

Разделы

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

Аффилиация

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