English
Lifting a GradeMaxOrder along a strictly monotone f preserves the max-element structure: if IsMax a then IsMax f(a).
Русский
Поднятие GradeMaxOrder по строго монотонной f сохраняет максимальность: если IsMax a, то IsMax f(a).
LaTeX
$$$\\forall a, IsMax(a) \\rightarrow IsMax(f(a))$$$
Lean4
/-- Lifts a graded order along a strictly monotone function. -/
abbrev liftLeft [GradeMaxOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b)
(hmax : ∀ a, IsMax a → IsMax (f a)) : GradeMaxOrder ℙ α :=
{ GradeOrder.liftLeft f hf hcovBy with isMax_grade := fun _ ha => hmax _ <| ha.grade _ }
-- See note [reducible non-instances]
