grade_covBy_grade_iff — Mathlib

English

Let 𝕆 be a preorder and α a linear order with GradeOrder 𝕆 α. The cover relation is preserved by grading: a ⋖ b iff grade 𝕆(a) ⋖ grade 𝕆(b).

Русский

Пусть 𝕆 — предпорядок, α — линейный порядок с градацией 𝕆 на α. Отношение покрытия сохраняется при градации: a ⋖ b тогда, когда grade 𝕆(a) ⋖ grade 𝕆(b).

LaTeX

$$$\\\\operatorname{CovBy}(\\\\operatorname{grade}_{\\\\mathcal{O}}(a), \\\\\\operatorname{grade}_{\\\\mathcal{O}}(b)) \\\\iff \\\\operatorname{CovBy}(a,b)$$$

Lean4

theorem grade_covBy_grade_iff : grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b :=
  (covBy_iff_lt_covBy_grade.trans <| and_iff_right_of_imp fun h => grade_lt_grade_iff.1 h.1).symm

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