English
Another formulation of transitivity for BlankRel; same content as above.
Русский
Еще одно формулирование транзитивности BlankRel; то же содержание, что и выше.
LaTeX
$$$\\forall l_1,l_2,l_3,\\ (BlankRel(l_1,l_2) \\land BlankRel(l_2,l_3)) \\Rightarrow BlankRel(l_1,l_3).$$$
Lean4
@[trans]
theorem trans {Γ} [Inhabited Γ] {l₁ l₂ l₃ : List Γ} : BlankRel l₁ l₂ → BlankRel l₂ l₃ → BlankRel l₁ l₃ :=
by
rintro (h₁ | h₁) (h₂ | h₂)
· exact Or.inl (h₁.trans h₂)
· rcases le_total l₁.length l₃.length with h | h
· exact Or.inl (h₁.above_of_le h₂ h)
· exact Or.inr (h₂.above_of_le h₁ h)
· rcases le_total l₁.length l₃.length with h | h
· exact Or.inl (h₁.below_of_le h₂ h)
· exact Or.inr (h₂.below_of_le h₁ h)
· exact Or.inr (h₂.trans h₁)
