preimage_iso — Mathlib

English

If t ⊆ β is an antichain and φ: α ≃o β is an order isomorphism, then φ^{-1}(t) is an antichain in α.

Русский

Пусть t ⊆ β является антицепочкой и φ: α ≃o β — изоморфизм порядков. Тогда φ^{-1}(t) — антицепочочка в α.

LaTeX

$$$IsAntichain(\le)(φ^{-1}t)$$$

Lean4

theorem preimage_iso [LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ≃o β) :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) :=
  preimage_relEmbedding ht _

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