instGradeOrderSubtypeMem — Mathlib

English

If 𝕆 is a preorder and α has a GradeOrder 𝕆 α, then the Flag s inherits a GradeOrder 𝕆 s via the natural lifting.

Русский

Если 𝕆 — предпорядок, а у α есть градиентный порядок 𝕆 α, то флаг s наследует GradeOrder 𝕆 s через естественное линейное вложение.

LaTeX

$$$ \\text{GradeOrder}(\\mathcal{O}, \\alpha) \\Rightarrow \\text{GradeOrder}(\\mathcal{O}, s). $$$

Lean4

instance [GradeOrder 𝕆 α] (s : Flag α) : GradeOrder 𝕆 s :=
  .liftRight _ (Subtype.strictMono_coe _) fun _ _ ↦ coe_covBy_coe.2

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