isChain_image — Mathlib

English

If f is monotone with respect to r and s, then the image of a chain under f is a chain in s.

Русский

Если функция монотонна относительно r и s, то образ цепи под действием f является цепью в s.

LaTeX

$$$\operatorname{IsChain}(r,c) \to (\forall x,y, r x y \to s (f x) (f y)) \to \operatorname{IsChain}(s, f[ c ])$$$

Lean4

theorem isChain_image [Preorder α] [Preorder β] {s : Set α} {f : α → β} (hf : Monotone f) (hs : IsChain (· ≤ ·) s) :
    IsChain (· ≤ ·) (f '' s) :=
  hs.image _ _ _ (fun _ _ a ↦ hf a)

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