English
Lifting a graded order along f : α → β yields a GradeOrder 𝕆 on α with grade := grade 𝕆 ∘ f.
Русский
Поднятие градации вдоль f: α → β порождает GradeOrder на α с grade = grade 𝕆 ∘ f.
LaTeX
$$$\\text{GradeOrder}_{𝕆}(α)\\; \\text{with } \\operatorname{grade} := \\operatorname{grade}_{𝕆} \\circ f$$$
Lean4
/-- Lifts a graded order along a strictly monotone function. -/
abbrev liftRight [GradeOrder 𝕆 β] (f : α → β) (hf : StrictMono f) (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder 𝕆 α
where
grade := grade 𝕆 ∘ f
grade_strictMono := grade_strictMono.comp hf
covBy_grade _ _
h :=
(hcovBy _ _ h).grade
_
-- See note [reducible non-instances]
