English
In products of preorders, a cover relation CovBy is characterized coordinatewise: a is CovBy b iff there exists an index i with a_i CovBy b_i and for all j ≠ i the coordinates satisfy an antisymmetry condition with respect to ≤.
Русский
В произведении предпорядков отношение CovBy характеризуется по координатам: a CovBy b тогда и только тогда, существует i, такое что a_i CovBy b_i, и для всех j ≠ i координаты удовлетворяют условию антисимметрии по отношению ≤.
LaTeX
$$$a \\<\\\\!\\\\! CovBy \\! b \\iff \\exists i, a_i \\<\\\\!\\\\! b_i \\land \\forall j \\neq i, AntisymmRel (\\\\le) (a_j) (b_j)$$$
Lean4
/-- A characterisation of the `CovBy` relation in products of preorders. See `Pi.covBy_iff` for the
(more common) version in products of partial orders.
-/
theorem covBy_iff_antisymmRel : a ⋖ b ↔ ∃ i, a i ⋖ b i ∧ ∀ j ≠ i, AntisymmRel (· ≤ ·) (a j) (b j) :=
by
constructor
· intro h
obtain ⟨j, hj⟩ := (Pi.lt_def.1 h.1).2
have : Nonempty ι := ⟨j⟩
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h.wcovBy
obtain rfl : i = j := by_contra fun this ↦ (hi j (Ne.symm this)).2.not_gt hj
exact ⟨i, covBy_iff_wcovBy_and_lt.2 ⟨h.wcovBy.eval i, hj⟩, hi⟩
rintro ⟨i, hi, h⟩
have : Nonempty ι := ⟨i⟩
refine covBy_iff_wcovBy_and_lt.2 ⟨wcovBy_iff_antisymmRel.2 ⟨i, hi.wcovBy, h⟩, ?_⟩
exact Pi.lt_def.2 ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hi.1.le) (h j · |>.1), i, hi.1⟩
