English
For a family of preorders indexed by ι, if CovBy holds pointwise, then there is an index i such that for all j ≠ i, AntisymmRel holds between a j and b j.
Русский
Для семейства предпорядков, индексируемого ι, если CovBy для функций a,b, то существует индекс i, такой что для всех j ≠ i выполняется AntisymmRel между a j и b j.
LaTeX
$$$ \text{exists_forall_antisymmRel_of_covBy}(h) : \exists i, \forall j \neq i,\; \text{AntisymmRel} (\le) (a j) (b j) $$$
Lean4
theorem _root_.WCovBy.eval (h : a ⩿ b) (i : ι) : a i ⩿ b i := by
classical
refine ⟨h.1 i, fun ci h₁ h₂ ↦ ?_⟩
have hcb : Function.update a i ci ≤ b := by simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j
refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)
simp [le_update_iff, h₂.not_ge]
