imp_of_mem_imp — Mathlib

English

If for all a,b with a,b ∈ l, R a b → S a b, then IsChain R l → IsChain S l.

Русский

Если для любых a,b в l, R a b → S a b, тогда IsChain R l ⇒ IsChain S l.

LaTeX

$$$ (\\forall a,b:\\alpha, a, b \\in l \\rightarrow R\\,a\\,b \\rightarrow S\\,a\\,b) \\rightarrow IsChain\\;R\\;l \\rightarrow IsChain\\;S\\;l$$$

Lean4

theorem imp_of_mem_imp {S : α → α → Prop} {l : List α} (H : ∀ a b : α, a ∈ l → b ∈ l → R a b → S a b)
    (p : IsChain R l) : IsChain S l :=
  p.imp_of_mem_tail_imp (H · · · <| mem_of_mem_tail ·)

Похожие утверждения