isChain_cons_of_isChain_cons_map — Mathlib

English

If there is a function f and a translation H translating S (on β) into R (on α) such that S(f a, f b) → R a b, then from IsChain S (f a :: map f l) we deduce IsChain R (a :: l).

Русский

Если существует функция f и переходное условие H: S(f(a), f(b)) → R(a,b), то из IsChain S (f a :: map f l) следует IsChain R (a :: l).

LaTeX

$$IsChain S (f a :: map f l) → (∀ 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_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b)
    {l : List α} (p : IsChain S (f a :: map f l)) : IsChain R (a :: l) :=
  ((isChain_cons_map f).1 p).imp H

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