English
If a list l is sorted by r, then for every k, every element x in take k l is related by r to every element y in drop k l.
Русский
Если список l упорядочен по r, то для каждого k любой элемент x из take k l связан relation r с любым элементом y из drop k l.
LaTeX
$$$$ \forall k:\n\mathbb{N},\ \forall x\in\mathrm{take}(k,l),\ \forall y\in\mathrm{drop}(k,l),\ r\ x\ y. $$$$
Lean4
theorem rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) {k : ℕ} {x y : α} (hx : x ∈ List.take k l)
(hy : y ∈ List.drop k l) : r x y :=
by
obtain ⟨iy, hiy, rfl⟩ := getElem_of_mem hy
obtain ⟨ix, hix, rfl⟩ := getElem_of_mem hx
rw [getElem_take, getElem_drop]
rw [length_take] at hix
exact h.rel_get_of_lt (Nat.lt_add_right _ (Nat.lt_min.mp hix).left)
