English
For a nonempty list l, there exists p1, p2 and l' with l'.Sorted in the < order and mapping by lineMap(p1,p2) yields l, if and only if l is Sbtw.
Русский
Для не пустого списка l существует p1, p2 и l' с l' упорядоченным по отношению < и отображением lineMap(p1,p2) в l, если и только если l удовлетворяет Sbtw.
LaTeX
$$$\\exists p_1,p_2,\\exists l'\\in List(\\mathbb{R}), l'.Sorted(\\lt) \\land l'.map(lineMap(p_1,p_2)) = l \\iff l.Sbtw(R)$$$
Lean4
theorem exists_map_eq_of_sorted_iff_sbtw [Nontrivial P] {l : List P} :
(∃ p₁ p₂ : P, p₁ ≠ p₂ ∧ ∃ l' : List R, l'.Sorted (· < ·) ∧ l'.map (lineMap p₁ p₂) = l) ↔ l.Sbtw R :=
by
refine ⟨fun ⟨p₁, p₂, hp₁p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
· subst hl'l
rw [(lineMap_injective _ hp₁p₂).list_sbtw_map_iff]
exact hl's.sbtw
· by_cases hl : l = []
· rcases exists_pair_ne P with ⟨p₁, p₂, hp₁p₂⟩
exact ⟨p₁, p₂, hp₁p₂, by simp [hl]⟩
· by_cases hlen : l.length = 1
· rw [length_eq_one_iff] at hlen
rcases hlen with ⟨p₁, rfl⟩
rcases exists_ne p₁ with ⟨p₂, hp₂p₁⟩
exact ⟨p₁, p₂, hp₂p₁.symm, [0], by simp⟩
· refine ⟨l.head hl, l.getLast hl, ?_⟩
rw [← exists_map_eq_of_sorted_nonempty_iff_sbtw hl] at h
simp only [hlen, false_or] at h
rcases h with ⟨l', hl's, hl'l, hl⟩
exact ⟨hl, l', hl's, hl'l⟩
