English
Lifting a GradeMaxOrder along f defines a GradeMaxOrder on 𝕆 with grade := grade 𝕆 ∘ f and preserves maxima.
Русский
Поднятие GradeMaxOrder по f задаёт GradeMaxOrder на 𝕆 с grade = grade 𝕆 ∘ f и сохраняет максимумы.
LaTeX
$$$[GradeMaxOrder 𝕆 β] \\Rightarrow [GradeMaxOrder 𝕆 α]$$$
Lean4
/-- Lifts a graded order along a strictly monotone function. -/
abbrev liftRight [GradeMaxOrder 𝕆 β] (f : α → β) (hf : StrictMono f) (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b)
(hmax : ∀ a, IsMax a → IsMax (f a)) : GradeMaxOrder 𝕆 α :=
{ GradeOrder.liftRight f hf hcovBy with isMax_grade := fun _ ha => (hmax _ ha).grade _ }
-- See note [reducible non-instances]
