instGradeMaxOrderSubtypeMem — Mathlib

English

If α has a GradeMaxOrder 𝕆 α, then the flag s inherits a GradeMaxOrder 𝕆 s.

Русский

Если у α имеется GradeMaxOrder 𝕆 α, то флаг s наследует GradeMaxOrder 𝕆 s.

LaTeX

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

Lean4

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

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