Additions to List.IsChain

Alphabet-generic List.IsChain facts not currently in mathlib, mirroring Mathlib/Data/List/Chain.lean. Candidates for upstreaming.

Main results

• List.isChain_top — every list is a chain for the always-true relation.
• List.isChain_cons_iff_of_forall_rel / List.isChain_append_singleton_iff_of_forall_rel — prepending/appending an element related to (or from) everything preserves IsChain.
• List.IsChain.and / List.isChain_and_iff — a chain for a conjunction relation is exactly a chain for each conjunct (the meet law; companion of List.IsChain.imp).

theorem List.isChain_top {α : Type u_1} (l : List α) : IsChain (fun (x x_1 : α) => True) l

Any list is a chain for the universal-true relation. The trivial case of IsChain for a relation that places no constraint on adjacent elements.

theorem List.isChain_cons_iff_of_forall_rel {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α} (h : ∀ (b : α), R a b) : IsChain R (a :: l) ↔ IsChain R l

Prepending an element that R-relates to everything preserves IsChain.

theorem List.isChain_append_singleton_iff_of_forall_rel {α : Type u_1} {R : α → α → Prop} {b : α} {l : List α} (h : ∀ (a : α), R a b) : IsChain R (l ++ [b]) ↔ IsChain R l

Appending an element that everything R-relates to preserves IsChain.

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

Two IsChain witnesses on the same list combine into a chain for the conjunction relation. The companion of mathlib's List.IsChain.imp.

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

A list is a chain for a conjunction relation iff it is a chain for each conjunct — the Iff strengthening of IsChain.and (the meet law for IsChain over its relation argument).