English
If s is an antichain in α with respect to ≤ and φ is an order isomorphism φ: α ≃o β, then φ''s is an antichain in β.
Русский
Если s является антицепочкой в α относительно ≤, и φ — изоморфизм порядков φ: α ≃o β, то φ''s — антицепочкой в β.
LaTeX
$$$IsAntichain(\le)(s) \Rightarrow IsAntichain(\le)(φ''s)$$$
Lean4
theorem image_iso [LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ≃o β) : IsAntichain (· ≤ ·) (φ '' s) :=
image_relEmbedding hs _