English
The covering relation on Lex(α×β) is described by the two alternatives: either first coordinates are equal and the second coordinates are in a covering relation, or first coordinates cover and the second coordinates are extreme (IsMax/IsMin).
Русский
Покрывающая связь на Lex(α×β) описывается двумя вариантами: либо первые координаты равны и вторые координаты удовлетворяют покрытию, либо первые координаты покрывают и вторые координаты — экстремумы (IsMax/IsMin).
LaTeX
$$$$ CovBy(a,b) \iff (Eq(a_1,b_1) ∧ CovBy(b_1,b_2)) \lor (CovBy(a_1,a_2) ∧ IsMax(b_1) ∧ IsMin(b_2)). $$$$
Lean4
theorem covBy_iff {a b : α ×ₗ β} :
a ⋖ b ↔
(ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ⋖ (ofLex b).2 ∨
(ofLex a).1 ⋖ (ofLex b).1 ∧ IsMax (ofLex a).2 ∧ IsMin (ofLex b).2 :=
toLex_covBy_toLex_iff
