preimage_embedding — Mathlib

English

If φ is an order-embedding from α to β and t is a chain in β, then φ⁻¹'(t) is a chain in α.

Русский

Если φ — впорядочивающее вложение из α в β и t — цепь в β, то φ⁻¹'(t) — цепь в α.

LaTeX

$$$ IsChain\\ (≤)\\ t \\rightarrow IsChain\\ (≤)\\ (φ^{-1}' t) $$$

Lean4

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

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