English
A is covered by B iff A < B and grade(A) is covered by grade(B) in the graded order.
Русский
A покрывает B тогда, когда A < B и grade(A) покрывает grade(B) в градуированном порядке.
LaTeX
$$$a \prec b \iff a < b \land \mathrm{grade}(a) \prec \mathrm{grade}(b).$$$
Lean4
theorem covBy_iff_lt_covBy_grade : a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b :=
⟨fun h => ⟨h.1, h.grade _⟩, And.imp_right fun h _ ha hb => h.2 (grade_strictMono ha) <| grade_strictMono hb⟩