instGradeBoundedOrderSubtypeMem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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