liftRight — Mathlib

English

Lifting a GradeBoundedOrder along f yields a GradeBoundedOrder on 𝕆 with grade := grade 𝕆 ∘ f.

Русский

Поднятие GradeBoundedOrder по f даёт GradeBoundedOrder на 𝕆 с grade = grade 𝕆 ∘ f.

LaTeX

$$$[GradeBoundedOrder 𝕆 β] \\Rightarrow [GradeBoundedOrder 𝕆 α]$$$

Lean4

/-- Lifts a graded order along a strictly monotone function. -/
abbrev liftRight [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.liftRight f hf hcovBy hmin, GradeMaxOrder.liftRight f hf hcovBy hmax with }

Похожие утверждения