preimage_embedding — Mathlib

English

Let t ⊆ β be an antichain with respect to ≤, and φ: α ↪o β an order-embedding. Then φ^{-1}(t) is an antichain in α.

Русский

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

LaTeX

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

Lean4

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

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