English
For a point p and a list l, the list p :: l satisfies Sbtw R iff l is pairwise with respect to Sbtw from p, l is Sbtw, and l is not a singleton [p].
Русский
Для точки p и списка l, список p :: l удовлетворяет Sbtw тогда и только тогда, когда l попарно различается относительно p, l удовлетворяет Sbtw и l ≠ [p].
LaTeX
$$$(p:\\,l).Sbtw(R) \\iff (l.P\,airwise(Sbtw(R,p)) \\land l.Sbtw(R) \\land l \\neq [p])$$$
Lean4
theorem sbtw_iff_triplewise_and_ne_pair [IsOrderedRing R] {l : List P} :
l.Sbtw R ↔ l.Triplewise (Sbtw R) ∧ ∀ a, l ≠ [a, a] :=
by
rw [List.Sbtw]
induction l with
| nil => simp
| cons head tail ih =>
rw [wbtw_cons, triplewise_cons]
refine ⟨fun h ↦ ?_, fun ⟨⟨hp, ht⟩, ha⟩ ↦ ⟨⟨hp.imp _root_.Sbtw.wbtw, ht.imp _root_.Sbtw.wbtw⟩, ?_⟩⟩
· rcases h with ⟨⟨hp, ht⟩, hpne⟩
refine ⟨⟨?_, ?_⟩, ?_⟩
· clear ih
induction tail with
| nil => simp
| cons head2 tail ih' =>
rw [pairwise_cons] at hp hpne hpne ⊢
refine ⟨fun a ha ↦ ⟨hp.1 a ha, ?_⟩, ?_⟩
· refine ⟨(hpne.1 head2 ?_).symm, hpne.2.1 a ha⟩
simp
· rw [wbtw_cons] at ht
grind [List.pairwise_iff_forall_sublist]
· rw [pairwise_cons] at hpne
exact (ih.1 ⟨ht, hpne.2⟩).1
· grind
· have ht' : tail.Wbtw R := ht.imp _root_.Sbtw.wbtw
simp only [ht', true_and, ht] at ih
rw [pairwise_cons, ih]
refine ⟨fun a ha' ↦ ?_, fun a ↦ ?_⟩
· rintro rfl
cases tail with
| nil => simp at ha'
| cons head2 tail =>
rw [pairwise_cons] at hp
rcases mem_cons.1 ha' with rfl | hat
·
cases tail with
| nil => simp at ha
| cons head3 tail => simpa using hp.1 head3
· simpa using hp.1 head hat
· rintro rfl
simp at hp
