English
For a₁,a₂ in α and b₁,b₂ in β, the covering relation between toLex(a₁,b₁) and toLex(a₂,b₂) is characterized by either a₁=a₂ and b₁ ⋖ b₂, or a₁ ⋖ a₂ with b₁ maximal and b₂ minimal in their respective coordinates.
Русский
Для a₁,a₂ ∈ α и b₁,b₂ ∈ β покрывающая связь между toLex(a₁,b₁) и toLex(a₂,b₂) задается либо a₁=a₂ и b₁ ⋖ b₂, либо a₁ ⋖ a₂ и b₁ является максимумом, а b₂ минимумом в своих координатах.
LaTeX
$$$$ \mathrm{CovBy}\left(\mathrm{toLex}(a_1,b_1), \mathrm{toLex}(a_2,b_2)\right) \iff (a_1=a_2 \land b_1 \prec b_2) \lor (a_1 \prec a_2 \land \mathrm{IsMax}(b_1) \land \mathrm{IsMin}(b_2)). $$$$
Lean4
/-- See also `monotone_fst_ofLex` for a version stated in terms of `Monotone`. -/
theorem monotone_fst [Preorder α] [LE β] (t c : α ×ₗ β) (h : t ≤ c) : (ofLex t).1 ≤ (ofLex c).1 := by
cases toLex_le_toLex.mp h with
| inl h' => exact h'.le
| inr h' => exact h'.1.le
