preimage_iso_iff — Mathlib

English

For an order isomorphism φ: α ≃o β and t ⊆ β, IsAntichain(≤) (φ^{-1}(t)) holds if and only if IsAntichain(≤) t.

Русский

Для изоморфизма порядков φ: α ≃o β и подмножества t ⊆ β верно IsAntichain(≤) (φ^{-1}(t)) тогда и только тогда IsAntichain(≤) t.

LaTeX

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

Lean4

theorem preimage_iso_iff [LE α] [LE β] {t : Set β} {φ : α ≃o β} :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) ↔ IsAntichain (· ≤ ·) t :=
  ⟨fun h => (φ.image_preimage t).subst (h.image_iso φ), fun h => h.preimage_iso _⟩

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