instOrderTopSubtypeMem

Mathlib.Order.Preorder.Chain

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

English

If α has OrderTop, the induced order on the subtype by membership is itself an OrderTop.

Русский

Если у α есть OrderTop, то обобщенная структура над подмножеством имеет верхнюю границу.

LaTeX

$$$[OrderTop α] \\\\rightarrow (s : Flag α) \\\\rightarrow OrderTop (Subtype (\\\\lambda x => SetLike.mem s x))$$$

Lean4

instance [OrderTop α] (s : Flag α) : OrderTop s :=
  Subtype.orderTop s.top_mem

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

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

Разделы

Аффилиация

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