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