isChain_cons_pmap_of_isChain_cons

English

If H translates R to S via f and p a predicate on α, then IsChain S (f a :: pmap f l hl) follows from IsChain R (a :: l).

Русский

Если H переводит R в S через f и есть p на α, тогда IsChain S (f a :: pmap f l hl) следует из IsChain R (a :: l).

LaTeX

$$∀ {l} (p : α → Prop) (f) (H : ∀ a b ha hb, R a b → S (f a ha) (f b hb)), IsChain R (a :: l) → IsChain S (f a ha :: pmap f l hl)$$

Lean4

theorem isChain_cons_pmap_of_isChain_cons {S : β → β → Prop} {p : α → Prop} {f : ∀ a, p a → β}
    (H : ∀ a b ha hb, R a b → S (f a ha) (f b hb)) {l : List α} {a} (ha) (hl₁ : IsChain R (a :: l))
    (hl₂ : ∀ a ∈ l, p a) : IsChain S (f a ha :: pmap f l hl₂) :=
  (isChain_cons_pmap f _ _).2 <| hl₁.imp_of_mem_imp (by grind)

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