covBy_iff_lt_covBy_grade — Mathlib

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⟩

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