image_embedding — Mathlib

English

If s is a chain in α with respect to ≤, and φ is an order-embedding from α to β, then the image φ''s is a chain in β with respect to ≤.

Русский

Если s — цепь в α относительно ≤, и φ — впорядочивающее вложение из α в β, тогда образ φ''s — цепь в β относительно ≤.

LaTeX

$$$ IsChain\\ (\\le)\\ s \\rightarrow IsChain\\ (\\le)\\ (\\phi '' s) $$$

Lean4

theorem image_embedding [LE α] [LE β] (hs : IsChain (· ≤ ·) s) (φ : α ↪o β) : IsChain (· ≤ ·) (φ '' s) :=
  image_relEmbedding hs _

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