instOrderBotSubtypeMem

Mathlib.Order.Preorder.Chain

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

English

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

Русский

Если у α есть OrderBot, то подмножество по членству образует OrderBot.

LaTeX

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

Lean4

instance [OrderBot α] (s : Flag α) : OrderBot s :=
  Subtype.orderBot s.bot_mem

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

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

Разделы

Аффилиация

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