English
For any list l, there exists p1, p2 and a real list l' sorted so that l'.map(lineMap p1 p2) = l if and only if l has Wbtw with respect to R.
Русский
Для любого списка l существует p1, p2 и l' — упорядоченный по возрастанию список в R так, что l'.map(lineMap p1 p2) = l тогда и только тогда, когда l имеет Wbtw по R.
LaTeX
$$$\\exists p_1,p_2,\\exists l'\\in List(R), l'.Sorted(\\cdot) \\land l'.map(lineMap(p_1,p_2)) = l \\iff Wbtw(R,l)$$$
Lean4
theorem exists_map_eq_of_sorted_iff_wbtw {l : List P} :
(∃ p₁ p₂ : P, ∃ l' : List R, l'.Sorted (· ≤ ·) ∧ l'.map (lineMap p₁ p₂) = l) ↔ l.Wbtw R :=
by
refine ⟨fun ⟨p₁, p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
· subst hl'l
exact Wbtw.map hl's.wbtw _
· by_cases hl : l = []
· exact ⟨AddTorsor.nonempty.some, AddTorsor.nonempty.some, [], by simp [hl]⟩
· exact ⟨l.head hl, l.getLast hl, (exists_map_eq_of_sorted_nonempty_iff_wbtw hl).2 h⟩
