English
Lifting a GradeBoundedOrder along a strictly monotone f yields a GradeBoundedOrder on α with the same grade-left structure.
Русский
Поднятие GradeBoundedOrder по строго монотонной f даёт GradeBoundedOrder на α с сохранением левой части структуры градации.
LaTeX
$$$[GradeBoundedOrder 𝕆 α] \\Rightarrow [GradeBoundedOrder 𝕆' α]$$$
Lean4
/-- Lifts a graded order along a strictly monotone function. -/
abbrev liftLeft [GradeBoundedOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b)
(hmin : ∀ a, IsMin a → IsMin (f a)) (hmax : ∀ a, IsMax a → IsMax (f a)) : GradeBoundedOrder ℙ α :=
{ GradeMinOrder.liftLeft f hf hcovBy hmin, GradeMaxOrder.liftLeft f hf hcovBy hmax with }
-- See note [reducible non-instances]
