isChain_map_of_isChain — Mathlib

English

If l is an R-chain and f maps α-elements to β with a relation S built to reflect R via f (i.e., S(f a, f b) whenever R a b), then map f l is an S-chain.

Русский

Пусть l — R-цепь, и f : α → β образует S-отношение через R, т.е. S(f(a), f(b)) следует из R(a,b). Тогда map f l является S-цепью.

LaTeX

$$IsChain R l → IsChain (\\lambda a b. R (f a) (f b)) l$$

Lean4

theorem isChain_map_of_isChain {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b)) {l : List α}
    (p : IsChain R l) : IsChain S (map f l) :=
  (isChain_map f).2 <| p.imp H

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