A member of a list that is pairwise related, related to one of its entries #
A candidate for Mathlib.Data.List.Pairwise: in a list l₁ ++ b :: l₂ that is pairwise related by
an asymmetric relation R, as a strictly increasing list is by <, a member a with R a b lies
in l₁.
Main statements #
List.mem_of_mem_append_cons_of_rel: a memberaofl₁ ++ b :: l₂, pairwise related by an asymmetricR, withR a bis a member ofl₁.
theorem
List.mem_of_mem_append_cons_of_rel
{α : Type u_1}
{R : α → α → Prop}
[Std.Asymm R]
{l₁ l₂ : List α}
{a b : α}
(h : Pairwise R (l₁ ++ b :: l₂))
(ha : a ∈ l₁ ++ b :: l₂)
(hab : R a b)
:
A member a with R a b of the list l₁ ++ b :: l₂, pairwise related by the asymmetric
relation R, is a member of l₁: it is not b, and R b x for the members x of l₂.