English
For indexed families of preorder, if CovBy holds, there exists an index i with antisymmetry across all other indices.
Русский
Для индексов семейства предорядков, если CovBy выполняется, существует индекс i с антисимметрией по всем другим индексам.
LaTeX
$$$ \text{exists_forall_antisymmRel_of_covBy}(h) : \exists i, \forall j, j \neq i \Rightarrow \text{AntisymmRel} (\cdot) (a j) (b j) $$$
Lean4
theorem exists_forall_antisymmRel_of_covBy (h : a ⋖ b) : ∃ i, ∀ j ≠ i, AntisymmRel (· ≤ ·) (a j) (b j) := by
classical
simp only [CovBy, Pi.lt_def, not_and, and_imp, forall_exists_index, not_exists] at h
obtain ⟨⟨hab, ⟨i, hi⟩⟩, h⟩ := h
refine ⟨i, fun j hj ↦ ?_⟩
let c : (i : ι) → α i := Function.update a i (b i)
have h₁ : c ≤ b := by simpa [update_le_iff, c] using fun k hk ↦ hab k
have h₂ : ¬c j < b j := h (by simp [c, hi.le]) i (by simpa [c]) h₁ j
exact ⟨hab j, by simpa [lt_iff_le_not_ge, hab j, c, hj] using h₂⟩
