English
If Rₐ is transitive, then SublistForall₂ Rₐ is a transitive relation on lists, i.e., composition of SublistForall₂-relations along a chain preserves the property.
Русский
Если Rₐ транзитивно, то SublistForall₂ Rₐ является транзитивным отношением на списках: композиция последовательных SublistForall₂-подотношений сохраняет свойство.
LaTeX
$$$$\\text{List.SublistForall₂.is\\_trans: } [IsTrans\\; α\\ R_\\alpha] \\Rightarrow \\text{IsTrans} (List\\; α) (List.SublistForall₂ R_\\alpha).$$$$
Lean4
instance is_trans [IsTrans α Rₐ] : IsTrans (List α) (SublistForall₂ Rₐ) :=
⟨fun a b c => by
revert a b
induction c with
| nil =>
rintro _ _ h1 h2
cases h2
exact h1
| cons _ _ ih =>
rintro a b h1 h2
obtain - | ⟨hbc, tbc⟩ | btc := h2
· cases h1
exact SublistForall₂.nil
· obtain - | ⟨hab, tab⟩ | atb := h1
· exact SublistForall₂.nil
· exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
· exact SublistForall₂.cons_right (ih _ _ atb tbc)
· exact SublistForall₂.cons_right (ih _ _ h1 btc)⟩
