image_iso — Mathlib

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 _

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