instGradeMinOrderSubtypeMem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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