image_embedding — Mathlib

English

If hs is an antichain with respect to ≤ on α and φ is an order-embedding α → β, then φ''s is an antichain with respect to ≤ on β.

Русский

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

LaTeX

$$$IsAntichain(\le, s) \rightarrow (\text{φ: } α \hookrightarrow o β) \rightarrow IsAntichain(\le, \operatorname{image}(\phi, s))$$$

Lean4

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

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