isChain_cons_map_of_isChain_cons — Mathlib

English

If IsChain R (a :: l) holds and every element of l satisfies p, then IsChain S (f a :: map f l) given H: ∀ a b ha hb, R a b → S (f a ha) (f b hb).

Русский

Если IsChain R (a :: l) и все элементы l удовлетворяют p, то IsChain S (f a :: map f l) при условии H: ∀ ha hb, R a b → S (f a ha) (f b hb).

LaTeX

$$IsChain R (a :: l) → (∀ a ∈ l, p a) → (∀ a b ha hb, R a b → S (f a ha) (f b hb)) → IsChain S (f a :: map f l)$$

Lean4

theorem isChain_cons_map_of_isChain_cons {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
    {l : List α} (p : IsChain R (a :: l)) : IsChain S (f a :: map f l) :=
  (isChain_cons_map f).2 <| p.imp H

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