image_embedding_iff — Mathlib

English

For φ: α ↪o β, a set s ⊆ α is an antichain if and only if its image φ''s ⊆ β is an antichain under ≤.

Русский

Для φ: α ↪o β и множества s ⊆ α, множество образов φ''s является антицепочкой тогда и только тогда, когда s сама является антицепочкой.

LaTeX

$$$IsAntichain(\le)(φ''s) \;\leftrightarrow\; IsAntichain(\le)s$$$

Lean4

theorem image_embedding_iff [LE α] [LE β] {φ : α ↪o β} : IsAntichain (· ≤ ·) (φ '' s) ↔ IsAntichain (· ≤ ·) s :=
  image_relEmbedding_iff

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