isChain_cons_of_isChain_cons_pmap

English

If f and H satisfy the stated implication from R to S, then from IsChain S (f a ha :: pmap f l hl) we obtain IsChain R (a :: l).

Русский

Если выполнено требуемое переходное условие от R к S, то IsChain S (f a ha :: pmap f l hl) ⇒ IsChain R (a :: l).

LaTeX

$$IsChain S (f a ha :: pmap f l hl) → (∀ a b ha hb, S (f a ha) (f b hb) → R a b) → IsChain R (a :: l)$$

Lean4

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

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