isChain_of_isChain_pmap — Mathlib

English

If pmap f l hl₁ is an S-chain and H maps S to R via f, then l is an R-chain.

Русский

Если pmap f l hl₁ образует S-цепь, и существует отображение H: S → R через f, то l является R-цепью.

LaTeX

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

Lean4

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

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