Lemmas about List.IsChain

Three List.IsChain facts whose List.Pairwise counterparts are in Init/Data/List/Pairwise.lean but which Mathlib/Data/List/Chain.lean lacks. [UPSTREAM] candidates for that file.

Main results

• List.isChain_of_forall: a relation that holds everywhere makes every list a chain, mirroring List.pairwise_of_forall.
• List.isChain_and_iff and List.IsChain.and: a chain for a conjunction of relations is exactly a chain for each conjunct, mirroring List.pairwise_and_iff and List.Pairwise.and.

theorem List.isChain_of_forall {α : Type u_1} {R : α → α → Prop} {l : List α} (H : ∀ (x y : α), R x y) : IsChain R l

theorem List.isChain_and_iff {α : Type u_1} {S T : α → α → Prop} {l : List α} : IsChain (fun (a b : α) => S a b ∧ T a b) l ↔ IsChain S l ∧ IsChain T l

theorem List.IsChain.and {α : Type u_1} {S T : α → α → Prop} {l : List α} (hS : IsChain S l) (hT : IsChain T l) : IsChain (fun (a b : α) => S a b ∧ T a b) l