English
For a nonempty list l, there exists l' with real entries, strictly increasing, such that l'.map(lineMap(head l, last l)) = l and (length condition) if and only if l.Sbtw holds.
Русский
Для не пустого списка l существует l' с вещественными элементами, строго возрастающим, такое что l'.map(lineMap(head l, last l)) = l и условие на длину эквивалентно, если и только если l.Sbtw.
LaTeX
$$$\\exists l'\\in List(\\mathbb{R}), l'.Sorted(\\cdot) \\land l'.map(lineMap(head(l), last(l))) = l \\land (length(l)=1 \\lor head(l) \\neq last(l)) \\iff l.Sbtw(R)$$$
Lean4
theorem exists_map_eq_of_sorted_nonempty_iff_sbtw {l : List P} (hl : l ≠ []) :
(∃ l' : List R,
l'.Sorted (· < ·) ∧
l'.map (lineMap (l.head hl) (l.getLast hl)) = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) ↔
l.Sbtw R :=
by
refine
⟨fun ⟨l', hl's, hl'l, hla⟩ ↦ ⟨(exists_map_eq_of_sorted_nonempty_iff_wbtw hl).1 ⟨l', (hl's.imp LT.lt.le), hl'l⟩, ?_⟩,
fun h ↦ ?_⟩
· rw [← hl'l]
rcases hla with hla | hla
· grind [List.pairwise_iff_forall_sublist]
· exact (hl's.imp LT.lt.ne).map _ fun _ _ ↦ (lineMap_injective _ hla).ne
· rw [List.Sbtw, ← exists_map_eq_of_sorted_nonempty_iff_wbtw hl] at h
rcases h with ⟨⟨l', hl's, hl'l⟩, hp⟩
refine ⟨l', ?_, hl'l, ?_⟩
· rw [← hl'l] at hp
have hp' : l'.Pairwise (· ≠ ·) := hp.of_map _ (by simp)
exact (pairwise_and_iff.2 ⟨hl's, hp'⟩).imp lt_iff_le_and_ne.2
·
cases l with
| nil => simp at hl
| cons head tail =>
simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
cases tail with
| nil => simp
| cons head2 tail =>
simp only [reduceCtorEq, false_or]
rw [pairwise_cons] at hp
refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
simp
