English
Let a and b be families a_i, b_i of elements indexed by ι in preordered sets (α_i). Then a is weakly covered by b if and only if there exists an index i such that a_i is weakly covered by b_i and for every j ≠ i the coordinates (a_j, b_j) are antisymmetric with respect to ≤ (i.e., AntisymmRel ≤ on a_j, b_j). In other words, the comparison between a and b is controlled by a single coordinate, while all other coordinates are equal up to antisymmetry.
Русский
Пусть a и b — семейства элементов, индексируемые ι, в предпорядках α_i. Тогда a ⩿ b эквивалентно существованию индекса i, для которого a_i ⩿ b_i, и для каждого j ≠ i выполняется AntisymmRel(≤)(a_j, b_j) (то есть эти координаты равны по антисимметрии). Другими словами, сравнение происходит по единой координате, остальные координаты равны (с учётом антисимметрии).
LaTeX
$$$a \\;⩿\\; b \\iff \\exists i, a_i \\;⩿\\; b_i \\land \\forall j \\neq i, AntisymmRel (\\le) (a_j) (b_j)$$$
Lean4
/-- A characterisation of the `WCovBy` relation in products of preorders. See `Pi.wcovBy_iff` for the
(more common) version in products of partial orders.
-/
theorem wcovBy_iff_antisymmRel [Nonempty ι] : a ⩿ b ↔ ∃ i, a i ⩿ b i ∧ ∀ j ≠ i, AntisymmRel (· ≤ ·) (a j) (b j) :=
by
constructor
· intro h
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_wcovBy h
exact ⟨i, h.eval _, hi⟩
rintro ⟨i, hab, h⟩
refine ⟨fun j ↦ (eq_or_ne j i).elim (· ▸ hab.1) (h j · |>.1), fun c hac hcb ↦ ?_⟩
have haci : a i < c i := by
obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac
exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦ ((lt_of_antisymmRel_of_lt (h j hj').symm hj).not_ge (hcb.le j)).elim
have hcbi : c i < b i := by
obtain ⟨hcb, j, hj⟩ := Pi.lt_def.1 hcb
exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦ ((lt_of_lt_of_antisymmRel hj (h j hj').symm).not_ge (hac.le j)).elim
exact hab.2 haci hcbi
