isChain_cons_map — Mathlib

English

For a fixed b in β and a list l of β, IsChain R of the list consisting of f(b) followed by map f l is equivalent to IsChain of b :: l with the relation R transported along f.

Русский

Для фиксированного b ∈ β и списка l по β условие IsChain R (f b :: map f l) эквивалентно IsChain по β для b :: l, с отношением, заданным через f.

LaTeX

$$IsChain R (f b :: map f l) \\iff IsChain (\\lambda a\\, b.\\, R (f a) (f b)) (b :: l)$$

Lean4

theorem isChain_cons_map (f : β → α) {l : List β} {b : β} :
    IsChain R (f b :: map f l) ↔ IsChain (fun a b : β => R (f a) (f b)) (b :: l) :=
  isChain_map f (l := b :: l)

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