English
Lifting a graded order along a strictly monotone map f : 𝕆 → ℙ yields a new GradeOrder on α with grade := f ∘ grade 𝕆; the construction preserves monotonicity and covariance of grades.
Русский
Поднятие градации вдоль строго монотонной карты f: 𝕆 → ℙ даёт новую градацию на α с grade = f ∘ grade 𝕆; сохранены монотонность и ковариантность градаций.
LaTeX
$$$\\text{GradeOrder}_{\\mathbb{P}}(\\\\alpha) = \\{ \\text{grade} = f \\circ \\text{grade}_{\\\\mathcal{O}}, \\ \\text{grade_strictMono} = \\text{hf} \\circ \\text{grade_strictMono}, \\ \\text{covBy\_grade} = \\dots \\}$$$
Lean4
/-- Lifts a graded order along a strictly monotone function. -/
abbrev liftLeft [GradeOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder ℙ α
where
grade := f ∘ grade 𝕆
grade_strictMono := hf.comp grade_strictMono
covBy_grade _ _
h :=
hcovBy _ _ <|
h.grade
_
-- See note [reducible non-instances]
