English
If a weak covBy relation holds between two indexed families, then there exists an index i such that for all j ≠ i, AntisymmRel holds between a j and b j; provided there is at least one index.
Русский
Если для двух функций существует слабое покрытие, то существует индекс i, при котором для всех j ≠ i выполняется AntisymmRel между a j и b j; при условии ненулевого множества индексов.
LaTeX
$$$ \text{exists_forall_antisymmRel_of_wcovBy}[Nonempty ](h) : \exists i, \forall j \neq i,\; \text{AntisymmRel} (\cdot) (a j) (b j) $$$
Lean4
theorem exists_forall_antisymmRel_of_wcovBy [Nonempty ι] (h : a ⩿ b) : ∃ i, ∀ j ≠ i, AntisymmRel (· ≤ ·) (a j) (b j) :=
by
rw [wcovBy_iff_covBy_or_le_and_le] at h
obtain h | h := h
· exact exists_forall_antisymmRel_of_covBy h
· inhabit ι
exact ⟨default, fun j hj ↦ ⟨h.left j, h.right j⟩⟩
