image_iso_iff — Mathlib

English

For s ⊆ α, IsAntichain(≤) (φ''s) holds if and only if IsAntichain(≤) s, when φ is an order isomorphism φ: α ≃o β.

Русский

Для подмножества s ⊆ α выполняется IsAntichain(≤) (φ''s) тогда и только тогда, когда IsAntichain(≤) s при условии, что φ — изоморфизм порядков φ: α ≃o β.

LaTeX

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

Lean4

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

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