instBoundedOrderSubtypeMem — Mathlib

English

If α has a bounded order, then the subtype on a flag also has a bounded order.

Русский

Если у α есть ограниченный порядок, то подтип флага имеет ограниченный порядок.

LaTeX

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

Lean4

instance [BoundedOrder α] (s : Flag α) : BoundedOrder s :=
  Subtype.boundedOrder s.bot_mem s.top_mem

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