English
For a in α and list l, (a :: l) is in s.subchain iff a ∈ s, l ∈ s.subchain, and every element of head(l) is greater than a.
Русский
Для элемента a и списка l: a :: l принадлежит s.subchain тогда и только тогда, когда a ∈ s, l ∈ s.subchain и каждый элемент головы списка l больше a.
LaTeX
$$$ (a :: l) \\in s.\\mathrm{subchain} \\iff a \\in s \\land l \\in s.\\mathrm{subchain} \\land \\forall b \\in l.\\mathrm{head?} \\; b \\Rightarrow a < b. $$$
Lean4
theorem cons_mem_subchain_iff : (a :: l) ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ b ∈ l.head?, a < b := by
simp only [subchain, mem_setOf_eq, forall_mem_cons, isChain_cons', and_left_comm, and_comm, and_assoc]
