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