isChain_pmap_of_isChain — Mathlib

English

If l is an α-chain with hl₁, every a in l has p(a), and if H maps R to S via f, then pmap f l hl₂ is an S-chain.

Русский

Если l — R-цепь по α, для каждого элемента l выполняется p(a), и если H переводит R в S через f, тогда pmap f l hl₂ образует S-цепь.

LaTeX

$$IsChain R (pmap f l hl₂)$$

Lean4

theorem isChain_pmap_of_isChain {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 α} (hl₁ : IsChain R l) (hl₂ : ∀ a ∈ l, p a) :
    IsChain S (pmap f l hl₂) :=
  (isChain_pmap f _).2 <| hl₁.imp_of_mem_imp (by grind)

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